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

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