English
If p ≠ 0 and f is injective, then the multiplicity of a as a root of p equals the multiplicity of f(a) as a root of p.map f.
Русский
Если p ≠ 0 и f инъективен, то кратность корня a в p совпадает с кратностью корня f(a) в p.map f.
LaTeX
$$rootMultiplicity(a, p) = rootMultiplicity(f(a), p.map f)$$
Lean4
theorem eq_rootMultiplicity_map {p : A[X]} {f : A →+* B} (hf : Function.Injective f) (a : A) :
rootMultiplicity a p = rootMultiplicity (f a) (p.map f) :=
by
by_cases hp0 : p = 0; · simp only [hp0, rootMultiplicity_zero, Polynomial.map_zero]
apply le_antisymm (le_rootMultiplicity_map ((Polynomial.map_ne_zero_iff hf).mpr hp0) a)
rw [le_rootMultiplicity_iff hp0, ← map_dvd_map f hf ((monic_X_sub_C a).pow _), Polynomial.map_pow, Polynomial.map_sub,
map_X, map_C]
apply pow_rootMultiplicity_dvd
