isConj_iff_conjugatesOf_eq — Mathlib

English

Two elements a and b are conjugate if and only if their sets of conjugates are equal.

Русский

Элементы a и b сопряжены тогда и только тогда, когда их множества сопряжённых элементов равны.

LaTeX

$$$IsConj(a,b) \iff \mathrm{conjugatesOf}(a) = \mathrm{conjugatesOf}(b)$$$

Lean4

theorem isConj_iff_conjugatesOf_eq {a b : α} : IsConj a b ↔ conjugatesOf a = conjugatesOf b :=
  ⟨IsConj.conjugatesOf_eq, fun h => by
    have ha := mem_conjugatesOf_self (a := b)
    rwa [← h] at ha⟩

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