map_toSubmodule — Mathlib

English

There is a linear equivalence between the submodule S viewed as a Submodule of A and the subalgebra S itself, via the natural embedding.

Русский

Существует линейное эквивалентное отображение между подмодулем S в A и самой подалгеброй S через естественную вложенность.

LaTeX

$$$S \cong_{\text{lin}} S$$$

Lean4

theorem map_toSubmodule {S : Subalgebra R A} {f : A →ₐ[R] B} :
    (toSubmodule <| S.map f) = S.toSubmodule.map f.toLinearMap :=
  SetLike.coe_injective rfl

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