commute_star_comm — Mathlib

English

Commutation with a star on the left is equivalent to commutation with the star on the right: Commute (star x) y ↔ Commute x (star y).

Русский

Сочетание слева со звездой эквивалентно сочетанию справа с звездой: Commute (star x) y ↔ Commute x (star y).

LaTeX

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

Lean4

theorem commute_star_comm {x y : R} : Commute (star x) y ↔ Commute x (star y) := by rw [← commute_star_star, star_star]

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