toLieEquiv_symm_apply

Mathlib.Algebra.Lie.OfAssociative

URI: https://scilib.ai/kg/mathlib#AlgEquiv.toLieEquiv_symm_apply

English

On application to an element x∈A1, the LieEquiv corresponding to AlgEquiv sends x to e x.

Русский

Применение к элементу x ∈ A1 даёт элемент e(x) в A2 под соответствием Lie.

LaTeX

$$$(\text{toLieEquiv}\ e) (x) = e(x)$$$

Lean4

@[simp]
theorem toLieEquiv_symm_apply (x : A₂) : e.toLieEquiv.symm x = e.symm x :=
  rfl

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

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

Разделы

Аффилиация

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