pow_sub_dvd_iterate_derivative_of_pow_dvd

English

If q^n ∣ p, then q^{n−m} ∣ derivative^[m] p for all m.

Русский

Если q^n делит p, то q^{n−m} делит производную^m p для любого m.

LaTeX

$$$$ q^{n-m} \mid \operatorname{derivative}^{m}(p) $$ при $q^n \mid p$$$

Lean4

theorem pow_sub_dvd_iterate_derivative_of_pow_dvd {p q : R[X]} {n : ℕ} (m : ℕ) (dvd : q ^ n ∣ p) :
    q ^ (n - m) ∣ derivative^[m] p := by
  induction m generalizing p with
  | zero => simpa
  | succ m ih =>
    rw [Nat.sub_succ, Function.iterate_succ']
    exact pow_sub_one_dvd_derivative_of_pow_dvd (ih dvd)

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