map_toSubmodule — Mathlib

English

The underlying submodule of map f S equals the image of S under the linear map induced by f.

Русский

Указанная подмодуля map f S равна образу S под линейным отображением, индуцированным f.

LaTeX

$$$ (\\mathrm{map}\, f\\, S)^{\\mathrm{toSubmodule}} = \\mathrm{Submodule.map}(\\mathrm{linearMap}\\ f)\\ S^{\\mathrm{toSubmodule}}. $$$

Lean4

theorem map_toSubmodule {S : NonUnitalSubalgebra R A} {f : F} :
    -- TODO: introduce a better coercion from `NonUnitalAlgHomClass` to `LinearMap`
    (map f S).toSubmodule = Submodule.map (LinearMapClass.linearMap f) S.toSubmodule :=
  SetLike.coe_injective rfl

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