submoduleMap_symm_apply — Mathlib

English

A linear equivalence between two modules restricts to a linear equivalence from any submodule p of the domain onto the image p.map e.

Русский

Линейное эквивалентное отображение между двумя модулей ограничивается до линейного эквивалентного отображения от любого подмодуля p области определения на образ p.map e.

LaTeX

$$$ e:\\, M \\simeq_\\sigma M_2 \\quad\\Rightarrow\\quad p \\xrightarrow{\\text{submoduleMap}} p.map e \\text{ is a linear equivalence }$$

Lean4

@[simp]
theorem submoduleMap_symm_apply (p : Submodule R M) (x : (p.map (e : M →ₛₗ[σ₁₂] M₂) : Submodule R₂ M₂)) :
    ↑((e.submoduleMap p).symm x) = e.symm x :=
  rfl

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