commute_iff_mul_inv_cancel_assoc — 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_assoc {u : Mˣ} {a : M} : Commute (↑u) a ↔ ↑u * (a * ↑u⁻¹) = a := by
  rw [u.commute_iff_mul_inv_cancel, mul_assoc]

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