toEnd_eq — Mathlib

English

A LieSubalgebra K of a Lie algebra L induces the same endomorphism action on its underlying module M as L does, via the inclusion K ↪ L.

Русский

Подалгебра K пространства L порождает ту же операцию к концу на модуле M через инклюзию K ↪ L.

LaTeX

$$$$ \text{toEnd}_R(K,M) \equiv \text{toEnd}_R(L,M) \quad \text{on } K.$$$$

Lean4

theorem toEnd_eq (K : LieSubalgebra R L) {x : K} : LieModule.toEnd R K M x = LieModule.toEnd R L M x :=
  rfl

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