Submodule.mkQ vs Submodule.Quotient.mk

Stream: mathlib4

[Nailin Guan]

I have a question here, why Submodule.Quotient.mk isn't marked private from the start? It is just a function not the linear function, and simp lemma on this simp mkQ to mk, making every theorem using compostion of linear function. I think the ideal way is like Ideal.Quotient.mk, although it makes dot notaion fail.

[Nailin Guan]

Also I think the name is also some how confusing as other quotient structures have their __.Quotient.mk the correct morphism.

[Nailin Guan]

So is everyone satisfied with changing Submodule.Quotient.mk into Submodule.mkQ as much as possible? If do, I would try to give a fix when I have some time.

[Nailin Guan]

I've opened #22269

[Nailin Guan]

However there are some parts that may need more careful design, so I am asking for some help here, thanks.