coe_toEnd — Mathlib

English

For a Lie submodule N ⊆ M, the endomorphism of N induced by x ∈ L is the same as the restriction of the endomorphism of M to N.

Русский

Для подмодуля Ли N ⊆ M эндоморфизм, соответствующий элементу x ∈ L, совпадает с ограничением эндоморфизма от M до N.

LaTeX

$$$\forall x \in L, \forall y \in N,\; (\mathrm{toEnd}_{R,L,N}(x)(y) = \mathrm{toEnd}_{R,L,M}(x)(y))$$$

Lean4

theorem coe_toEnd (N : LieSubmodule R L M) (x : L) (y : N) : (toEnd R L N x y : M) = toEnd R L M x y :=
  rfl

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