Drop MulEquivClass?

Stream: mathlib4

[Yury G. Kudryashov]

What do you think about using [EquivLike F M N] [MulHomClass F M N] instead of [EquivLike F M N] [MulEquivClass F M N]? (fixed after @Edward van de Meent 's reply)

[Yury G. Kudryashov]

See #14284

[Edward van de Meent]

i think you mean [EquivLike F M N] [MulEquivClass F M N] rather than [FunLike F M N] [MulEquivClass F M N]?

[Edward van de Meent]

i think that this should be fine, although i imagine we might want to keep it at least as an alias?

[Ruben Van de Velde]

No, the topic was about dropping MulEquivClass

[Yaël Dillies]

That trick works for MulEquiv but it doesn't work for Homeomorph (since a continuous bijection is not necessarily a homeomorphism)

[Yaël Dillies]

So I'm not sure we should start following that pattern given that it doesn't generalise

[Edward van de Meent]

Ruben Van de Velde said:

No, the topic was about dropping MulEquivClass

i understand that, my first point is about the fact that MulEquivClass takes an EquivLike parameter.

My second point is that i think people will expect MulEquivClass to exist because it fits the pattern of XHomClass and XEquivClass, so we should at least have some kind of way to tell them that "something is going on in this case"

[Yury G. Kudryashov]

We should decide what to do and either drop MulEquivClass and other algebraic *EquivClasses, or drop the comments in the code suggesting to do this.

[Jireh Loreaux]

Let's drop the comments in the code.