English
If p ≠ 0 and the hypotheses hold with an inductive prime version, then n < p.rootMultiplicity t under the refined nonzero divisor condition.
Русский
Если p ≠ 0 и выполняются условия в переработанном виде, то выполняется неравенство n < p.rootMultiplicity t при хорошем условии, что числа m меньших чем n не делят ноль.
LaTeX
$$$$n < p.rootMultiplicity\,t$$$$
Lean4
theorem lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors' {p : R[X]} {t : R} {n : ℕ} (h : p ≠ 0)
(hroot : ∀ m ≤ n, (derivative^[m] p).IsRoot t) (hnzd : ∀ m ≤ n, m ≠ 0 → (m : R) ∈ nonZeroDivisors R) :
n < p.rootMultiplicity t :=
by
apply lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors h hroot
clear hroot
induction n with
| zero =>
simp only [Nat.factorial_zero, Nat.cast_one]
exact Submonoid.one_mem _
| succ n ih =>
rw [Nat.factorial_succ, Nat.cast_mul, mul_mem_nonZeroDivisors]
exact ⟨hnzd _ le_rfl n.succ_ne_zero, ih fun m h ↦ hnzd m (h.trans n.le_succ)⟩
