toEnd_mk — Mathlib

English

For a LieSubalgebra K with element x ∈ L, the endomorphism corresponding to x in K coincides with that for x in L.

Русский

Для x ∈ L скобка в K и в L дают одинаковый эндоморфизм.

LaTeX

$$$$ \text{toEnd}_R(K,M)\langle x, \mathrm{hx} \rangle = \text{toEnd}_R(L,M)\; x,$$ where hx denotes membership of x in K.$$

Lean4

@[simp]
theorem toEnd_mk (K : LieSubalgebra R L) {x : L} (hx : x ∈ K) :
    LieModule.toEnd R K M ⟨x, hx⟩ = LieModule.toEnd R L M x :=
  rfl

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