commute_iff_inv_mul_cancel — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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