conj_iff — Mathlib

English

Conjugating both elements of a commuting pair by h preserves commutativity: h a h^{-1} and h b h^{-1} commute if and only if a and b commute.

Русский

Сопряжение каждой переменной пары, которая коммутирует, сохраняет коммутативность: h a h^{-1} и h b h^{-1} коммутируют тогда и только тогда, когда a и b коммутируют.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
protected theorem conj_iff (h : G) : Commute (h * a * h⁻¹) (h * b * h⁻¹) ↔ Commute a b :=
  SemiconjBy.conj_iff

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