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