English
For any t, the root multiplicity of the expanded polynomial satisfies: rootMultiplicity(t, expand_R(p^n,f)) = p^n · rootMultiplicity(t^{p^n}, f).
Русский
Для любой точки t кратность корня после расширения по p^n равна p^n умножить на кратность корня в f при t^{p^n}.
LaTeX
$$$$\mathrm{rootMultiplicity}(t, \mathrm{expand}_R(p^n,f))=p^n\cdot \mathrm{rootMultiplicity}(t^{p^n}, f)$$$$
Lean4
theorem rootMultiplicity_expand_pow :
(expand R (p ^ n) f).rootMultiplicity r = p ^ n * f.rootMultiplicity (r ^ p ^ n) :=
by
obtain rfl | h0 := eq_or_ne f 0; · simp
obtain ⟨g, hg, ndvd⟩ := f.exists_eq_pow_rootMultiplicity_mul_and_not_dvd h0 (r ^ p ^ n)
rw [dvd_iff_isRoot, ← eval_X (x := r), ← eval_pow, ← isRoot_comp, ← expand_eq_comp_X_pow] at ndvd
conv_lhs =>
rw [hg, map_mul, map_pow, map_sub, expand_X, expand_C, map_pow, ← sub_pow_expChar_pow, ← pow_mul, mul_comm,
rootMultiplicity_mul_X_sub_C_pow
(expand_ne_zero (expChar_pow_pos R p n) |>.mpr <| right_ne_zero_of_mul <| hg ▸ h0),
rootMultiplicity_eq_zero ndvd, zero_add]
