conj — Mathlib

English

If a and b commute, then their conjugates by any element h also commute; i.e., h a h^{-1} and h b h^{-1} commute.

Русский

Если a и b коммутируют, то их конъюгаты на произвольном h, h a h^{-1} и h b h^{-1}, тоже коммутируют.

LaTeX

$$$ \\text{Commute } a b \\Rightarrow \\text{Commute } (h a h^{-1}) (h b h^{-1}) $$$

Lean4

@[to_additive]
protected theorem conj (comm : Commute a b) (h : G) : Commute (h * a * h⁻¹) (h * b * h⁻¹) :=
  (Commute.conj_iff h).mpr comm

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