Elementary linear-equivalence transport

Transport of submodule stability through an intertwining linear equivalence. Symmetry of a linear automorphism agrees with inversion in its group structure.

theorem LinearEquiv.symm_eq_inv {R : Type u_1} {V : Type u_2} [Semiring R] [AddCommMonoid V] [Module R V] (e : V ≃ₗ[R] V) : e.symm = e⁻¹

Symmetry of a linear automorphism is its group inverse.

theorem LinearEquiv.mem_of_preserves_map {R : Type u_1} {V : Type u_2} {W : Type u_3} [Semiring R] [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module R W] (e : V ≃ₗ[R] W) (p : Submodule R V) (q : Submodule R W) (hmap : Submodule.map (↑e) p = q) (f : V → V) (g : W → W) (hcomm : ∀ (x : V), e (f x) = g (e x)) (hstable : ∀ {y : W}, y ∈ q → g y ∈ q) {x : V} (hx : x ∈ p) : f x ∈ p

Transport stability of a mapped submodule through an intertwining linear equivalence.