quotient inconsistency

Stream: maths

[Kevin Buzzard]

Just noticed when preparing teaching that G →* G ⧸ N is quotient_group.mk' N and V →ₗ[k] V ⧸ X is submodule.mkq X. Should quotient_group be removed or should there be a quotient_module, or is there a logical reason for this apparent inconsistency?

[Jireh Loreaux]

Our naming around quotients is a mess everywhere I think. The nice thing about submodule.mkq is that you can use dot notation I guess, so that's a point in its favor.