what does doset even mean

Stream: mathlib4

[Kevin Buzzard]

I recently discovered that mathlib has docs#Doset.doset . Can anyone guess what it means without clicking? I propose we rename it to what mathematicians call it. Or is this standard terminology? I'd never heard of it.

It means "Double coset". Can we rename to DoubleCoset?
```

[Edward van de Meent]

even reading the spoiler i couldn't figure it out, i had to go to the docs and expand the equation... i agree we should call it what mathematicians call it (unless of course there is a clearer way to express the concept)

[Damiano Testa]

I agree that it should be called what the spoiler says: without context (and maybe even with context!), I would have never guessed its meaning.

[Eric Wieser]

Maybe this should be a new threshold for whether mathlib should have something; introduce it with a silly name, and if no one complains within 3 years then maybe mathlib didn't need it after all!

[Kevin Buzzard]

I need it for FLT, and that was how I discovered it!

[Damiano Testa]

And given that Chris authored the file, I imagine that they wanted it for similar reasons!

[Kevin Buzzard]

Yes, we're both thinking about Hecke operators right now.

[Eric Wieser]

(I was kidding, I don't think mathlib should be pruned of things that no one currently wants)

[Johan Commelin]

I confess that I know what a Doset.doset is, without looking at the spoiler...

[Johan Commelin]

But I reviewed the PR that introduced it... so maybe you should take this data point with a grain of salt

[Ben Eltschig]

Eric Wieser said:

Maybe this should be a new threshold for whether mathlib should have something; introduce it with a silly name, and if no one complains within 3 years then maybe mathlib didn't need it after all!

I know you were kidding, but I'd still like to mention that they find use in the construction of universal orbifold coverings too, so I will need them if/when I get to formalising that. I don't think I would have easily found them under that name though, if I hadn't seen this post...