English
If derivative f = 0 and p ≠ 0 in a ring of characteristic p, then expand p (contract p f) = f.
Русский
Если производная f равна 0 и p ≠ 0 в кольце с характеристикой p, то expand_p(contract_p f) = f.
LaTeX
$$$$\mathrm{expand}_R(p)\bigl(\mathrm{contract}_p f\bigr)=f$$$$
Lean4
theorem derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors {p : R[X]} {t : R} (hpt : Polynomial.IsRoot p t)
(hnzd : (p.rootMultiplicity t : R) ∈ nonZeroDivisors R) :
(derivative p).rootMultiplicity t = p.rootMultiplicity t - 1 :=
by
by_cases h : p = 0
· simp only [h, map_zero, rootMultiplicity_zero]
obtain ⟨g, hp, hndvd⟩ := p.exists_eq_pow_rootMultiplicity_mul_and_not_dvd h t
set m := p.rootMultiplicity t
have hm : m - 1 + 1 = m := Nat.sub_add_cancel <| (rootMultiplicity_pos h).2 hpt
have hndvd : ¬(X - C t) ^ m ∣ derivative p :=
by
rw [hp, derivative_mul, dvd_add_left (dvd_mul_right _ _), derivative_X_sub_C_pow, ← hm, pow_succ, hm,
mul_comm (C _), mul_assoc, dvd_cancel_left_mem_nonZeroDivisors (monic_X_sub_C t |>.pow _ |>.mem_nonZeroDivisors)]
rw [dvd_iff_isRoot, IsRoot] at hndvd ⊢
rwa [eval_mul, eval_C, mul_left_mem_nonZeroDivisors_eq_zero_iff hnzd]
have hnezero : derivative p ≠ 0 := fun h ↦ hndvd (by rw [h]; exact dvd_zero _)
exact
le_antisymm (by rwa [rootMultiplicity_le_iff hnezero, hm])
(rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero _ t hnezero)
