IsConj — Mathlib

English

Conjugacy is defined by existence of a unit c with b = c a c^{-1}.

Русский

Конъугированность определяется существованием единицы c, такой что b = c a c^{-1}.

LaTeX

$$$IsConj(a,b) := \\exists c : \\alpha^{\\times}, \\\\operatorname{SemiconjBy}(c, a, b)$$$

Lean4

/-- We say that `a` is conjugate to `b` if for some unit `c` we have `c * a * c⁻¹ = b`. -/
def IsConj (a b : α) :=
  ∃ c : αˣ, SemiconjBy (↑c) a b

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