splits_minpoly — Mathlib

English

If the base extension is normal, then the minimal polynomial of c splits over L: Splits (algebraMap K L) c.minpoly.

Русский

Если основание K ⊆ L нормальное, то минимальный полином c распадается над L: Splits (algebraMap K L) c.minpoly.

LaTeX

$$$\\text{Splits}(\\operatorname{algebraMap} K L, c.minpoly)$$$

Lean4

theorem splits_minpoly [n : Normal K L] (c : ConjRootClass K L) : Splits (algebraMap K L) c.minpoly :=
  by
  induction c
  rw [minpoly_mk]
  exact n.splits _

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