Notation for sums (misunderstood?)

Stream: new members

[Philippe Duchon]

I am trying to understand how to work with infinite sums in Mathlib, and it seems I am not even writing things correctly - I cannot even write a sum with the dedicated notation.

import Mathlib

section Series
variable {α β K: Type*} [CommSemiring K] [TopologicalSpace K] (f: α → K)

#check tsum f
#check Σ' i, (f i: K)
#check Σ' i, f i
#check Σ' (i:ℕ), i
#check Σ' (i:ℕ), (0:ℕ)
end Series

The #check tsum f command works, but in all others Lean complains that the terms I am trying to sum have the wrong type.

Is there some missing import, or some other subtle thing I misunderstood?

[Rémy Degenne]

You are not using the right sum sign. You should use the one you get by typing \sum

[Rémy Degenne]

In the code above, you used the sign \Sigma instead.

[Philippe Duchon]

Huh! Thanks a lot. The glyphs do look awfully similar though...

Is there also a special character for the comma? I changed the \Sigmas to \sums, and Lean is now complaining about "missing end of character litteral". Oops, just inserted a space between the sum sign and the prime.

[Philippe Duchon]

Just to make this a bit clearer: when browsing the documentation (on github), is there a simple way of finding out what the characters are? (Or, in VScode, but the info doesn't seem to appear when the character is part of the infoview, just when it's in the file window; so it's not much help when one it typing the wrong characters)

[Rémy Degenne]

You can copy the character from the documentation into vscode and then put your cursor over it to see how to type it. I don't know a faster way.

[Philippe Duchon]

OK, nothing smarter then. Thanks!