Stream: math-comp users

Topic: Definition of \sum_i \sum_j \sum_k...


view this post on Zulip Julien Puydt (Sep 05 2022 at 11:47):

I'm looking for the definitions of \sum_i, \sum_j and \sum_k... they are used in a few libs - always in mathcomp and not stdlib-based code - but I couldn't grep my way to the definition. It looks like it's a \sum_(i < n.+1) ; in any case it's apparently incompatible with a \sum_(0 <= i < n.+1).

view this post on Zulip Reynald Affeldt (Sep 05 2022 at 12:00):

big_mkord makes a link between both sums

view this post on Zulip Pierre Roux (Sep 05 2022 at 12:01):

The notation is defined here https://github.com/math-comp/math-comp/blob/c66a532bc7878c366acfe5203083fb3dcbb31d3e/mathcomp/ssreflect/bigop.v#L617-L618
It is also overriden here https://github.com/math-comp/math-comp/blob/c66a532bc7878c366acfe5203083fb3dcbb31d3e/mathcomp/algebra/ssralg.v#L6179-L6180
So you are mostly right, \sum_i basically means "infer the range from the type of i".

view this post on Zulip Pierre Roux (Sep 05 2022 at 12:02):

For instance if i : 'I_n the range is 0,...,n-1. And indeed, since \sum_(0 <= i < n) is a summation with i : nat, no range can be inferred from the type nat.

view this post on Zulip Julien Puydt (Sep 05 2022 at 13:12):

@Reynald Affeldt Indeed big_mkord helped me make the translation.

@Pierre Roux It's both introduced and overriden... thanks.


Last updated: Jan 29 2023 at 19:02 UTC