toLieHom_id

Mathlib.Algebra.Lie.OfAssociative

URI: https://scilib.ai/kg/mathlib#AlgHom.toLieHom_id

English

The identity algebra hom id_R,A lifts to the identity LieHom on A.

Русский

Идентичный алгебро-гомоморфизм id_R,A переходит в идентичный LieHom.

LaTeX

$$$$\big(\mathrm{AlgHom.id}\, R\, A\big)^{\mathrm{Lie}} = \mathrm{LieHom.id}.$$$$

Lean4

@[simp]
theorem toLieHom_id : (AlgHom.id R A : A →ₗ⁅R⁆ A) = LieHom.id :=
  rfl

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

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

Разделы

Аффилиация

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