English
An associative ring gives rise to a Lie ring by taking the bracket to be the ring commutator.
Русский
Ассоциативное кольцо образует Ли-кольцо, если определить скобку как коммутатор кольца.
LaTeX
$$$ \\text{If } A \\text{ is a ring, then } \\lbrack x,y \\rbrack = xy - yx \\text{ defines a Lie bracket on } A. $$$
Lean4
/-- An associative ring gives rise to a Lie ring by taking the bracket to be the ring commutator. -/
instance (priority := 100) ofAssociativeRing : LieRing A
where
add_lie _ _ _ := by simp only [Ring.lie_def, right_distrib, left_distrib]; abel
lie_add _ _ _ := by simp only [Ring.lie_def, right_distrib, left_distrib]; abel
lie_self := by simp only [Ring.lie_def, forall_const, sub_self]
leibniz_lie _ _ _ := by simp only [Ring.lie_def, mul_sub_left_distrib, mul_sub_right_distrib, mul_assoc]; abel
