natSepDegree_ne_zero — Mathlib

English

If a polynomial is non-constant, its separable degree is non-zero.

Русский

Если многочлен ненулевой константы, его сепарабельная степень ненулевая.

LaTeX

$$$ \operatorname{natSepDegree}(f) \neq 0 $ whenever $ \operatorname{natDegree}(f) \neq 0 $$$

Lean4

/-- A non-constant polynomial has non-zero separable degree. -/
theorem natSepDegree_ne_zero (h : f.natDegree ≠ 0) : f.natSepDegree ≠ 0 :=
  by
  rw [natSepDegree, ne_eq, Finset.card_eq_zero, ← ne_eq, ← Finset.nonempty_iff_ne_empty]
  use rootOfSplits _ (SplittingField.splits f) (ne_of_apply_ne _ h)
  classical
  rw [Multiset.mem_toFinset, mem_aroots]
  exact ⟨ne_of_apply_ne _ h, map_rootOfSplits _ (SplittingField.splits f) (ne_of_apply_ne _ h)⟩

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