English
For nonzero p, rootMultiplicity a p equals the Nat.find of the finiteMultiplicity object (as before).
Русский
Для ненулевого p корневую кратность p по a можно выразить через Nat.find конечной величины множества.
LaTeX
$$$$ \\operatorname{rootMultiplicity}(a, p) = \\operatorname{Nat.find}(\\text{finiteMultiplicity } X - C a\, p). $$$$
Lean4
theorem rootMultiplicity_eq_nat_find_of_nonzero [DecidableEq R] {p : R[X]} (p0 : p ≠ 0) {a : R} :
-- `decidableDvdMonic` can't be an instance, so we inline it here.
letI : DecidablePred fun n : ℕ => ¬(X - C a) ^ (n + 1) ∣ p := fun n =>
have := decidableDvdMonic p ((monic_X_sub_C a).pow (n + 1))
inferInstanceAs (Decidable ¬_)
rootMultiplicity a p = Nat.find (finiteMultiplicity_X_sub_C a p0) :=
by
dsimp [rootMultiplicity]
cases Subsingleton.elim ‹DecidableEq R› (Classical.decEq R)
rw [dif_neg p0]
