natSepDegree_eq_natDegree_iff — Mathlib

English

If f is separable, then its separable degree equals its degree.

Русский

Если f сепарабельный, то сепарабельная степень равна степени f.

LaTeX

$$$ f.Separable \Rightarrow \operatorname{natSepDegree}(f) = \operatorname{natDegree}(f) $$$

Lean4

/-- The separable degree of a non-zero polynomial is equal to its degree if and only if
it is separable. -/
theorem natSepDegree_eq_natDegree_iff (hf : f ≠ 0) : f.natSepDegree = f.natDegree ↔ f.Separable := by
  classical
  simp_rw [← card_rootSet_eq_natDegree_iff_of_splits hf (SplittingField.splits f), rootSet_def, Finset.coe_sort_coe,
    Fintype.card_coe]
  rfl

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