maxTrivEquiv_of_equiv_symm_eq_symm

Mathlib.Algebra.Lie.Abelian

URI: https://scilib.ai/kg/mathlib#LieModule.maxTrivEquiv_of_equiv_symm_eq_symm

English

The center of a Lie algebra is an abelian Lie algebra.

Русский

Center Ли-алгебры является абелевой Ли-алгеброй.

LaTeX

$$$\\text{IsLieAbelian }(\\text{center }R L)$.$$

Lean4

@[simp]
theorem maxTrivEquiv_of_equiv_symm_eq_symm (e : M ≃ₗ⁅R,L⁆ N) : (maxTrivEquiv e).symm = maxTrivEquiv e.symm :=
  rfl

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

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

Разделы

Аффилиация

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