natSepDegree_eq_zero_iff — Mathlib

English

A polynomial has zero separable degree if and only if it has zero degree.

Русский

Многочлен имеет нулевую сепарабельную степень тогда и только тогда, когда его нулевая степень равна нулю.

LaTeX

$$$ \operatorname{natSepDegree}(f) = 0 \iff \operatorname{natDegree}(f) = 0 $$$

Lean4

/-- A polynomial has zero separable degree if and only if it is constant. -/
theorem natSepDegree_eq_zero_iff : f.natSepDegree = 0 ↔ f.natDegree = 0 :=
  ⟨(natSepDegree_ne_zero f).mtr, natSepDegree_eq_zero f⟩

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