map_top_submodule — Mathlib

English

The image of the top submodule under the inverse of the linear equivalence is the top submodule: (⊤ : Submodule R E).map (linearEquiv R A E).symm = ⊤.

Русский

Образ верхнего подпространства через обратную линейную эквивалентность равен верхнему подпространству: (⊤ : Submodule R E).map (linearEquiv R A E).symm = ⊤.

LaTeX

$$$ (\top : \mathrm{Submodule}_R E).map \big( (linearEquiv R A E)\!\text{.symm} \big) = \top $$$

Lean4

theorem map_top_submodule {R : Type*} [Semiring R] [AddCommGroup E] [Module R E] :
    (⊤ : Submodule R E).map (linearEquiv R A E).symm = ⊤ :=
  Submodule.map_eq_top_iff.mpr rfl

Похожие утверждения