units_inv_right_iff — Mathlib

English

Commute a with the inverse unit is equivalent to commuting with the unit: Commute a ↑u^{-1} ↔ Commute a u.

Русский

Коммутирует ли a с инверсией единицы, эквивалентно тому, что a коммутирует с самой единицей: Commute a ↑u^{-1} ↔ Commute a u.

LaTeX

$$$Commute(a, ↑u^{-1}) \Leftrightarrow Commute(a, u)$$$

Lean4

@[to_additive (attr := simp)]
theorem units_inv_right_iff : Commute a ↑u⁻¹ ↔ Commute a u :=
  SemiconjBy.units_inv_right_iff

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