ofAssociativeAlgebra — Mathlib

English

An associative algebra A over a commutative ring R carries a natural Lie algebra structure with bracket given by the ring commutator: ⁅x,y⁆ = xy − yx for x,y ∈ A.

Русский

Ассоциативная алгебра A над кольцом R обладает естественной структурой Lie-алгебры: скобка ⁅x,y⁆ = xy − yx для x,y ∈ A.

LaTeX

$$$$[x,y] = xy - yx \quad (x,y \in A).$$$$

Lean4

/-- An associative algebra gives rise to a Lie algebra by taking the bracket to be the ring
commutator. -/
instance (priority := 100) ofAssociativeAlgebra : LieAlgebra R A where
  lie_smul t x
    y := by
    rw [LieRing.of_associative_ring_bracket, LieRing.of_associative_ring_bracket, Algebra.mul_smul_comm,
      Algebra.smul_mul_assoc, smul_sub]

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