isConjRoot_iff_orbitRel — Mathlib

English

For a normal extension, y is a conjugate root of x iff x,y lie in the same orbit of the Galois group action.

Русский

При нормальном расширении y является сопряжённым корнем x тогда, когда x и y лежат в одной орбите действия Галуа.

LaTeX

$$$IsConjRoot(K, x, y) \iff MulAction.orbitRel (L \simeq_K L) L\; x\; y$$$

Lean4

/-- Let `L / K` be a normal field extension. For any two elements `x` and `y` in `L`, `y` is a
conjugate root of `x` if and only if `x` and `y` falls in the same orbit of the action of Galois
group.
-/
theorem isConjRoot_iff_orbitRel [Normal K L] {x y : L} : IsConjRoot K x y ↔ MulAction.orbitRel (L ≃ₐ[K] L) L x y :=
  (isConjRoot_iff_exists_algEquiv)

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