Precedence issue

Stream: mathlib4

[Patrick Massot]

In docs#LinearMap.quotKerEquivRange, I find it a little bit sad to need parentheses around the quotient. Is there a good reason for the quotient notation to have such a low precedence?

[Eric Wieser]

It seems odd to me that the precedence of ≃ₗ[ is different to that of ≃[

[Eric Wieser]

It seems some of our isomorphisms are :25, and others :50

[Patrick Massot]

I understand that Equiv is data but I think the least surprising behavior would still to have the same precedence as equality.

[Patrick Massot]

And I having that giving the quotient symbol a precedence comparable to the division precedence is also the most unsurprising.