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).

`big_mkord`

makes a link between both sums

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".

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.

@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