natSepDegree_eq_natDegree — Mathlib

English

A restatement of the previous equivalence using a dot notation alias.

Русский

Переформулировка предыдущего равенства через точечную запись.

LaTeX

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

Lean4

/-- Same as `Polynomial.natSepDegree_eq_natDegree_of_separable`, but enables the use of
dot notation. -/
theorem natSepDegree_eq_natDegree (h : f.Separable) : f.natSepDegree = f.natDegree :=
  natSepDegree_eq_natDegree_of_separable f h

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