English
Let A be a ring. The multiplication on A is commutative if and only if every pair of elements commute, equivalently the Lie bracket [a, b] := ab − ba vanishes for all a, b ∈ A.
Русский
Пусть A — кольцо. Умножение на A коммутативно тогда и только тогда, когда для любых элементов a, b ∈ A выполняется [a, b] = 0, где [a, b] = ab − ba.
LaTeX
$$$\\left(\\forall a,b\\in A\\, ab=ba\\right) \\iff \\left(\\forall a,b\\in A\\, [a,b]=0\\right),\\quad \\text{with } [a,b]:=ab-ba.$$$
Lean4
theorem commutative_ring_iff_abelian_lie_ring {A : Type v} [Ring A] :
Std.Commutative (α := A) (· * ·) ↔ IsLieAbelian A :=
by
have h₁ : Std.Commutative (α := A) (· * ·) ↔ ∀ a b : A, a * b = b * a := ⟨fun h => h.1, fun h => ⟨h⟩⟩
have h₂ : IsLieAbelian A ↔ ∀ a b : A, ⁅a, b⁆ = 0 := ⟨fun h => h.1, fun h => ⟨h⟩⟩
simp only [h₁, h₂, LieRing.of_associative_ring_bracket, sub_eq_zero]
