English
If the characteristic of R at p is defined and p ≠ 0, and the derivative of f is zero, then expanding after contracting yields f: expand_R(p)(contract_p f) = f.
Русский
Если характеристика R по p определена и p ≠ 0, и производная f равна нулю, то после сжатия и расширения снова получим f: expand_p(contract_p f) = f.
LaTeX
$$$$\mathrm{expand}_R(p)\bigl(\mathrm{contract}_p f\bigr)=f$$$$
Lean4
theorem expand_contract [CharP R p] [NoZeroDivisors R] {f : R[X]} (hf : Polynomial.derivative f = 0) (hp : p ≠ 0) :
expand R p (contract p f) = f := by
ext n
rw [coeff_expand hp.bot_lt, coeff_contract hp]
split_ifs with h
· rw [Nat.div_mul_cancel h]
· rcases n with - | n
· exact absurd (dvd_zero p) h
have := coeff_derivative f n
rw [hf, coeff_zero, zero_eq_mul] at this
rcases this with h' | _
· rw [h']
rename_i _ _ _ h'
rw [← Nat.cast_succ, CharP.cast_eq_zero_iff R p] at h'
exact absurd h' h
