commute_star_star — Mathlib

English

The star of two elements commutes if and only if the original elements commute: Commute (star x) (star y) ↔ Commute x y.

Русский

Звезда двух элементов коммутирует тогда и только тогда, когда сами элементы коммутиируют: Commute (star x) (star y) ↔ Commute x y.

LaTeX

$$$$ \operatorname{Commute}(\star x, \star y) \iff \operatorname{Commute}(x, y). $$$$

Lean4

@[simp]
theorem commute_star_star {x y : R} : Commute (star x) (star y) ↔ Commute x y :=
  semiconjBy_star_star_star

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