commute_iff_mul_inv_cancel — Mathlib

English

For any unit u and element a, Commute(u, a) implies u a u^{-1} = a.

Русский

Для любой единицы u и элемента a, если u и a коммутируют, то u a u^{-1} = a.

LaTeX

$$$\\\\operatorname{Commute}(\\uparrow u, a) \\\\Rightarrow \\\\ u a u^{-1} = a$$$

Lean4

@[to_additive]
theorem _root_.Units.commute_iff_mul_inv_cancel {u : Mˣ} {a : M} : Commute (↑u) a ↔ ↑u * a * ↑u⁻¹ = a := by
  rw [Units.mul_inv_eq_iff_eq_mul, Commute, SemiconjBy]

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