coe_ad

Mathlib.Algebra.Lie.OfAssociative

URI: https://scilib.ai/kg/mathlib#LieSubalgebra.coe_ad

English

For a Lie subalgebra H ⊆ L, the adjoint action ad_H x on H coincides with the adjoint action ad_L x on L, for x ∈ H and y ∈ H.

Русский

Для подалгебры H ⊆ L и x,y ∈ H, действие ad_H x на H совпадает с ad_L x на L.

LaTeX

$$$\forall H\subseteq L,\; \mathrm{ad}_H(x)(y) = \mathrm{ad}_L(x)(y)$ for all $x,y\in H$$$

Lean4

theorem coe_ad (H : LieSubalgebra R L) (x y : H) : (ad R H x y : L) = ad R L x y :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru