natSepDegree_le_natDegree — Mathlib

English

For any polynomial f, the separable degree is at most its degree: natSepDegree(f) ≤ natDegree(f).

Русский

Для любого многочлена выполняется неравенство: natSepDegree(f) ≤ natDegree(f).

LaTeX

$$$ \operatorname{natSepDegree}(f) \le \operatorname{natDegree}(f) $$$

Lean4

/-- The separable degree of a polynomial is smaller than its degree. -/
theorem natSepDegree_le_natDegree : f.natSepDegree ≤ f.natDegree :=
  by
  have := f.map (algebraMap F f.SplittingField) |>.card_roots'
  rw [← aroots_def, natDegree_map] at this
  classical exact (f.aroots f.SplittingField).toFinset_card_le.trans this

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