English
For a normal extension, two elements have the same minimal polynomial over F iff one lies in the orbit of the other under the automorphism group of the extension.
Русский
Для нормального расширения два элемента имеют одинаковый минимальный многочлен над F тогда и только тогда, когда один принадлежит орбитальному перемещению другого по группе автоморфизмов расширения.
LaTeX
$$minpoly F x = minpoly F y ⇔ x ∈ Orbit_{(E ≃_F E)}(y)$$
Lean4
/-- If `E/Kᵢ/F` are towers of fields with `E/F` normal then we can lift
an algebra isomorphism `ϕ : K₁ ≃ₐ[F] K₂` to `ϕ.liftNormal E : E ≃ₐ[F] E`. -/
noncomputable def liftNormal [Normal F E] : E ≃ₐ[F] E :=
AlgEquiv.ofBijective (χ.toAlgHom.liftNormal E) (AlgHom.normal_bijective F E E _)
