tower_top_of_normal — Mathlib

English

If E is normal over F, then K is normal over E in a tower F ⊆ K ⊆ E with IsScalarTower.

Русский

Если E нормально над F, то K нормально над E в башне F ⊆ K ⊆ E при наличии IsScalarTower.

LaTeX

$$$\text{If } [\text{Normal } F E],\ \text{then } \mathrm{Normal} K E$ (in a tower with IsScalarTower).$$

Lean4

@[stacks 09HN]
theorem tower_top_of_normal [h : Normal F E] : Normal K E :=
  normal_iff.2 fun x => by
    obtain ⟨hx, hhx⟩ := h.out x
    rw [algebraMap_eq F K E] at hhx
    exact
      ⟨hx.tower_top,
        Polynomial.splits_of_splits_of_dvd (algebraMap K E) (Polynomial.map_ne_zero (minpoly.ne_zero hx))
          ((Polynomial.splits_map_iff (algebraMap F K) (algebraMap K E)).mpr hhx)
          (minpoly.dvd_map_of_isScalarTower F K x)⟩

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