coe_toLieHom

Mathlib.Algebra.Lie.OfAssociative

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

English

Underlying map of the LieHom associated to an AlgHom equals the original algebra hom’s map.

Русский

Базовая карта сопутствующего LieHom совпадает с исходной картой AlgHom.

LaTeX

$$$$((f : A \to_{R} B)^{\mathrm{Lie}}) = f.$$$$

Lean4

@[simp]
theorem coe_toLieHom : ((f : A →ₗ⁅R⁆ B) : A → B) = f :=
  rfl

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

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

Разделы

Аффилиация

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