toEnd_comp_mk' — Mathlib

English

The composition of the endomorphism actions with mk' commutes with mk' and LieModule.toEnd.

Русский

Композиция действий концевых отображений с mk' коммутирует с mk' и действием Ли-алгебры.

LaTeX

$$toEnd_comp_mk' (x : L) : LieModule.toEnd R L (M ⧸ N) x ∘ₗ mk' N = mk' N ∘ₗ LieModule.toEnd R L M x$$

Lean4

theorem toEnd_comp_mk' (x : L) : LieModule.toEnd R L (M ⧸ N) x ∘ₗ mk' N = mk' N ∘ₗ LieModule.toEnd R L M x :=
  rfl

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