Transporting a quotient along a linear equivalence

This small helper packages the quotient equivalence induced when a linear equivalence carries one submodule exactly onto another.

def MagnitudeConjecture.LinearEquiv.quotientOfMapEq {R : Type u} [Ring R] {M : Type v} {N : Type w} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) (p : Submodule R M) (q : Submodule R N) (h : Submodule.map (↑e) p = q) : (M ⧸ p) ≃ₗ[R] N ⧸ q

A linear equivalence carrying p onto q descends to the corresponding quotient modules.

@[simp]

theorem MagnitudeConjecture.LinearEquiv.quotientOfMapEq_mk {R : Type u} [Ring R] {M : Type v} {N : Type w} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) (p : Submodule R M) (q : Submodule R N) (h : Submodule.map (↑e) p = q) (x : M) : (quotientOfMapEq e p q h) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (e x)