notation

Stream: condensed mathematics

[Johan Commelin]

I've been replacing the sequences of constants c_ and c' by κ and κ' everywhere. So now the Lean code matches the blueprint and Analytic.pdf again. (Over there, the change was made a couple of weeks ago.)
The main reason: there is a constant $c_0$ that has mostly nothing to do with the constants $c_1, c_2, \ldots$. So now this distinction is a lot more clear.

[Johan Commelin]

To make the (old) confusion worse... in Lean the sequence of constants c_ of course was indexed by nat and so there was also a c_ 0. In practice c_ 0 = 1, and that's why there is no $c_0$ in the sequence of constants in the PDF. But you can see why it's a good idea to distinguish the notations :smiley:

[Peter Scholze]

I'm very bad with choosing nonconflicting notation. Any auxiliary index is an $i$, no matter whether other $i$'s are around, etc... Thanks for the disambiguation!

[Johan Commelin]

Well, Lean can actually handle multiple variables with the same name in the same context... so technically there is no problem

[Johan Commelin]

But you might need to jump through several hoops later on to explain to it which of the different is you want to use

[Peter Scholze]

Oh, how does Lean do that? That's cool

[Johan Commelin]

It has unique identifiers behind the scenes

[Johan Commelin]

Actually, variables are implemented using de Bruijn indices (which are unrelated to the de Bruijn factor)

[Johan Commelin]

https://en.wikipedia.org/wiki/De_Bruijn_index

[Johan Commelin]

But there is some interface on top of that which allows human-readable variable names