toLieEquiv — Mathlib

English

The symmetry of lieConj is preserved under application: the symm code yields same result as applying symm of e.

Русский

Сохранение симметрии lieConj под применением: результат симм равен применению симм.

LaTeX

$$$e.lieConj.symm = e.symm.lieConj$$$

Lean4

/-- An equivalence of associative algebras is an equivalence of associated Lie algebras. -/
def toLieEquiv : A₁ ≃ₗ⁅R⁆ A₂ :=
  { e.toLinearEquiv with
    toFun := e.toFun
    map_lie' := fun {x y} => by
      have : e.toEquiv.toFun = e := rfl
      simp_rw [LieRing.of_associative_ring_bracket, this, map_sub, map_mul] }

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