English
In NoZeroSMulDivisors ℕ R, natDegree hasseDeriv n p equals natDegree p minus n.
Русский
При отсутствии нулевых делителей по действию ℕ на R, natDegree(hasseDeriv_n p) = natDegree(p) − n.
LaTeX
$$$\operatorname{natDegree}(\mathrm{hasseDeriv}_n p) = \operatorname{natDegree}(p) - n$$$
Lean4
theorem natDegree_hasseDeriv [NoZeroSMulDivisors ℕ R] (p : R[X]) (n : ℕ) :
natDegree (hasseDeriv n p) = natDegree p - n :=
by
rcases lt_or_ge p.natDegree n with hn | hn
· simpa [hasseDeriv_eq_zero_of_lt_natDegree, hn] using (tsub_eq_zero_of_le hn.le).symm
· refine map_natDegree_eq_sub ?_ ?_
· exact fun h => hasseDeriv_eq_zero_of_lt_natDegree _ _
·
classical
simp only [ite_eq_right_iff, Ne, natDegree_monomial, hasseDeriv_monomial]
intro k c c0 hh
rw [← nsmul_eq_mul, smul_eq_zero, Nat.choose_eq_zero_iff] at hh
exact (tsub_eq_zero_of_le (Or.resolve_right hh c0).le).symm
