map_one — Mathlib

English

map f of the unit submodule equals the unit submodule: map f.toLinearMap (1) = 1.

Русский

образ единицы через линейное отображение сопоставления равен единице: map f.toLinearMap (1) = 1.

LaTeX

$$$ \operatorname{Submodule.map} f^{\mathrm{toLinearMap}} (1) = 1 $$$

Lean4

protected theorem map_one {A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') :
    map f.toLinearMap (1 : Submodule R A) = 1 := by
  ext
  simp

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