commute_iff_lie_eq — Mathlib

English

Let R be a nonunital nonassociative ring. For all x, y in R, x and y commute if and only if their Lie bracket [x, y] is zero, i.e. [x, y] = 0.

Русский

Пусть R — кольцо без единицы и без необходимости ассоциативности. Для любых x, y ∈ R верно: x и y коммутируют тогда и только тогда, когда их скобка Ли [x, y] равна нулю, т.е. [x, y] = 0.

LaTeX

$$$xy = yx \Longleftrightarrow [x,y] = 0$$$

Lean4

theorem commute_iff_lie_eq {x y : R} : Commute x y ↔ ⁅x, y⁆ = 0 :=
  sub_eq_zero.symm

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