conjugatesOf_eq — Mathlib

English

If a and b are conjugate, their sets of conjugates coincide: conjugatesOf(a) = conjugatesOf(b).

Русский

Если a и b сопряжены, их множества сопряжённых элементов совпадают.

LaTeX

$$$IsConj\;a\;b \Rightarrow \mathrm{conjugatesOf}(a) = \mathrm{conjugatesOf}(b)$$$

Lean4

theorem conjugatesOf_eq {a b : α} (ab : IsConj a b) : conjugatesOf a = conjugatesOf b :=
  Set.ext fun _ => ⟨fun ag => ab.symm.trans ag, fun bg => ab.trans bg⟩

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