natSepDegree_eq_natDegree_of_separable

English

As a variant, if f.Separable, then natSepDegree = natDegree (dot notation equivalent).

Русский

Как вариант, если f.Separable, то natSepDegree = natDegree (эквивалент через точку).

LaTeX

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

Lean4

/-- If a polynomial is separable, then its separable degree is equal to its degree. -/
theorem natSepDegree_eq_natDegree_of_separable (h : f.Separable) : f.natSepDegree = f.natDegree :=
  (natSepDegree_eq_natDegree_iff f h.ne_zero).2 h

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