natSepDegree — Mathlib

English

The separable degree of a polynomial is defined as the number of distinct roots in its splitting field.

Русский

Сепарабельная степень многочлена определяется как число различных корней в поле распада.

LaTeX

$$$ \operatorname{natSepDegree}(f) = |(f.aroots(f.SplittingField)).toFinset| \,\text{cardinality} $$$

Lean4

/-- The separable degree `Polynomial.natSepDegree` of a polynomial is a natural number,
defined to be the number of distinct roots of it over its splitting field.
This is similar to `Polynomial.natDegree` but not to `Polynomial.degree`, namely, the separable
degree of `0` is `0`, not negative infinity. -/
def natSepDegree : ℕ :=
  (f.aroots f.SplittingField).toFinset.card

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