toEnd_comp_subtype_mem — Mathlib

English

For a LieSubmodule N and x ∈ L, the image of N under the endomorphism associated to x is contained in N.

Русский

Для подмодуля Ли N и x ∈ L образ N под действием x входит в N.

LaTeX

$$$(N : Submodule R M).map (\mathrm{toEnd}_{R,L,M} x) \le N$$$

Lean4

theorem toEnd_comp_subtype_mem (m : M) (hm : m ∈ (N : Submodule R M)) :
    (toEnd R L M x).comp (N : Submodule R M).subtype ⟨m, hm⟩ ∈ (N : Submodule R M) := by simpa using N.lie_mem hm

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