natSepDegree_eq — Mathlib

English

The separable degree of X^n is 0 for n = 0 and 1 otherwise.

Русский

Разделяемая степень X^n равна 0 при n = 0 и 1 при n > 0.

LaTeX

$$$ (X^n).\operatorname{natSepDegree} = \begin{cases}0, & n=0 \\ 1, & n>0 \end{cases} $$$

Lean4

/-- If a polynomial has separable contraction, then its separable degree is equal to the degree of
the given separable contraction. -/
theorem natSepDegree_eq {q : ℕ} [ExpChar F q] (hf : f.HasSeparableContraction q) : f.natSepDegree = hf.degree :=
  hf.isSeparableContraction.natSepDegree_eq

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