Julien Puydt (Sep 05 2022 at 11:47): 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).
Reynald Affeldt (Sep 05 2022 at 12:00):big_mkord makes a link between both sums
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".
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.
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.
Notification Bot (Sep 05 2022 at 20:17):Julien Puydt has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC