Making `ideal.quotient` reducible (or deleted altogether?)

Stream: general

[Anne Baanen]

I'm working with ideals that have finite quotients, so my variables look like (I : ideal R) [fintype (ideal.quotient I)]. When I want to apply some lemma defined for submodule quotients, I get a missing instance error for fintype (submodule.quotient I). Since docs#ideal.quotient is defined to equal docs#submodule.quotient, this error goes away if we make ideal.quotient reducible.

Do you know any objection to making ideal.quotient reducible, or even deleting it entirely? (Dot notation is smart enough to interpret I.quotient as submodule.quotient I even if I : ideal R.)

[Kevin Buzzard]

First vector spaces, now this :-) I have caught myself in the past writing submodule R R