ofSubmodule'_symm_apply — Mathlib

English

If a linear equivalence identifies a submodule with the bottom submodule, the submodule must be bottom.

Русский

Если линейное эквивалентность идентифицирует подмодуль с нулевым подмодулем, то такой подмодуль должен быть нулевым.

LaTeX

$$eq_bot_of_equiv (e : p ≃_l[R] (⊥ : Submodule R₂ M₂)) : p = ⊥$$

Lean4

@[simp]
theorem ofSubmodule'_symm_apply [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂) (x : U) :
    ((f.ofSubmodule' U).symm x : M) = f.symm (x : M₂) :=
  rfl

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