English
SplittingFieldAux n f splits f in the corresponding extension field; i.e., f factors completely there.
Русский
SplittingFieldAux n f разворачивает f в соответствующем расширении; полное разложение в этом поле.
LaTeX
$$$\\text{Splits}(\\text{algebraMap }K \\; \\text{SplittingFieldAux }n f)\\; f$$$
Lean4
protected theorem splits (n : ℕ) :
∀ {K : Type u} [Field K], ∀ (f : K[X]) (_hfn : f.natDegree = n), Splits (algebraMap K <| SplittingFieldAux n f) f :=
Nat.recOn (motive := fun n =>
∀ {K : Type u} [Field K], ∀ (f : K[X]) (_hfn : f.natDegree = n), Splits (algebraMap K <| SplittingFieldAux n f) f) n
(fun {_} _ _ hf =>
splits_of_degree_le_one _ (le_trans degree_le_natDegree <| hf.symm ▸ WithBot.coe_le_coe.2 zero_le_one))
fun n ih {K} _ f hf =>
by
rw [← splits_id_iff_splits, algebraMap_succ, ← map_map, splits_id_iff_splits, ←
X_sub_C_mul_removeFactor f fun h => by rw [h] at hf; cases hf]
exact splits_mul _ (splits_X_sub_C _) (ih _ (natDegree_removeFactor' hf))
