toLieEquiv_apply — Mathlib

English

An isomorphism of associative algebras induces a Lie algebra isomorphism between their associated Lie algebras.

Русский

Изоморфизм ассоциативных алгебр индуцирует изоморфизм Ли-алгебр между соответствующими алгебрами Ли.

LaTeX

$$$\text{toLieEquiv} : A_1 \simeq_{\text{Lie}} A_2$ from $A_1 \simeq_{\text{Alg}} A_2$$$

Lean4

@[simp]
theorem toLieEquiv_apply (x : A₁) : e.toLieEquiv x = e x :=
  rfl

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