Mbar → Lbar

Stream: condensed mathematics

[Johan Commelin]

Breaking change: all occurences of Mbar in filenames and Lean code have been changed to Lbar.

[Johan Commelin]

The reason: @Filippo A. E. Nuccio introduced the notation ℒ r S for laurent_measures r S. This is denoted $ℳ(S, ℤ((T))_r)$ in Analytic.pdf. But I like the short ℒ notation a lot. And Lbar is a quotient of this space. It also emphasises that it is two steps away from real_measures p S which is denoted $ℳ_p(S)$ in Analytic.pdf.

[Johan Commelin]

I will push the same change to the blueprint once CI finishes compiling LTE

[Peter Scholze]

Nice!

By the way, isn't one practical reason to not overdo abbreviations that search-and-replace is much safer on longer names?

[Johan Commelin]

I guess that's true.

[Filippo A. E. Nuccio]

Yes, it seems a good point.

[Johan Commelin]

In Lean 4 it will be possible to say "take this Lean name foo, and rename it to bar in the entire project"

[Filippo A. E. Nuccio]

Wow

[Patrick Massot]

Note this is a completely standard thing to expect in any modern programming language, but Lean 3 never reached that level of polish because it was very much a research project, not a finished thing.