Hard to type definitions in representation theory

Stream: mathlib4

[Yaël Dillies]

I found IsCocycle₁/IsCocycle₂ really hard to type in search tools like the docs or grep. I considered renaming them to IsOneCocycle/IsTwoCocycle before realising this would precisely revert #26546! In other parts of the library, we have banished hard to type characters in definition names (eg docs#MeasureTheory.Memℒp became docs#MeasureTheory.MemLp), why is representation theory sailing against the wind here?
cc @Johan Commelin, @Amelia Livingston

[Alfredo Moreira-Rosa]

if you are on linux (gnome), you can use the compose key (usually right ctrl) :

• [compose] _ [NUM] to have subscripts
• [compose] ^ [NUM] to have superscripts

it's even faster to type than the bindings in vs code using \

[Violeta Hernández]

I recently added docs#Ordinal.invVeblen₁ and docs#Ordinal.invVeblen₂. I wasn't aware subscripts were considered an issue :frown:

[Violeta Hernández]

...and by the fact docs# doesn't work with them, they certainly are

[Violeta Hernández]

I'd like one of two things to happen:
a) adapt our tooling so that it works with subscripts better (e.g. have the docs recognize 1 as ₁)
b) specify in our naming convention that subscripts are disallowed, or at least highly discouraged

[Eric Wieser]

Violeta Hernández said:

...and by the fact docs# doesn't work with them, they certainly are

docs#Ordinal.invVeblen₁ works fine for me :)

[Kevin Buzzard]

Perhaps the context should include the information that there have been changes to the regex in the last couple of hours :-)

[Patrick Massot]

I really don't think we should encourage people to have misconfigured computers. It's important that Lean is usable in any case, but here we are discussing non essential uses. If you can't type subscript numbers that's a problem with your configuration, not with Mathlib.

[Michael Rothgang]

... but then we should also teach users how to configure their computer "properly".

[Michael Rothgang]

This could e.g. be a subtle link to an explanation page on the loogle webpage. Lean's learning curve is already steep, let's try to not make it too much harder.

[Alfredo Moreira-Rosa]

Learning how to type subscript for your computer platform is about 10 mn research on the internet. That was the first thing i did when i started with lean because vs code \ helper required too much typing for my liking.
I don't think 10mn is too much of a barrier.

[Filippo A. E. Nuccio]

But I am unsure I understand your comment: using the vs code helper requires two strokes: \ + 1, while GNOME compose requires three: [compose] + _ + 1. Or am I missing something?