minpoly_eq_iff_mem_orbit — Mathlib

English

An iSup of normal subextensions is normal.

Русский

iSup нормальных подрасширений нормален.

LaTeX

$$Normal F (⨆ i, t i)$$

Lean4

theorem minpoly_eq_iff_mem_orbit [h : Normal F E] {x y : E} :
    minpoly F x = minpoly F y ↔ x ∈ MulAction.orbit (E ≃ₐ[F] E) y :=
  by
  refine ⟨fun he ↦ ?_, fun ⟨f, he⟩ ↦ he ▸ minpoly.algEquiv_eq f y⟩
  obtain ⟨φ, hφ⟩ := exists_algHom_of_splits_of_aeval (normal_iff.mp h) (he ▸ minpoly.aeval F x)
  exact ⟨AlgEquiv.ofBijective φ (φ.normal_bijective F E E), hφ⟩

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