English
Let p be a monic polynomial with deg p > 0 and q be a nonzero polynomial over a ring R. Then the multiplicity of p in q is finite.
Русский
Пусть p — монический полином над кольцом R и deg p > 0, а q — ненулевой полином над R. Тогда кратность p в q конечна.
LaTeX
$$$ 0 < \deg p \;\wedge\; \operatorname{Monic}(p) \wedge q \neq 0 \;\Longrightarrow\; \nu_p(q) < \infty $$$
Lean4
theorem finiteMultiplicity_of_degree_pos_of_monic (hp : (0 : WithBot ℕ) < degree p) (hmp : Monic p) (hq : q ≠ 0) :
FiniteMultiplicity p q :=
have zn0 : (0 : R) ≠ 1 :=
haveI := Nontrivial.of_polynomial_ne hq
zero_ne_one
⟨natDegree q, fun ⟨r, hr⟩ => by
have hp0 : p ≠ 0 := fun hp0 => by simp [hp0] at hp
have hr0 : r ≠ 0 := fun hr0 => by subst hr0; simp [hq] at hr
have hpn1 : leadingCoeff p ^ (natDegree q + 1) = 1 := by simp [show _ = _ from hmp]
have hpn0' : leadingCoeff p ^ (natDegree q + 1) ≠ 0 := hpn1.symm ▸ zn0.symm
have hpnr0 : leadingCoeff (p ^ (natDegree q + 1)) * leadingCoeff r ≠ 0 := by
simp only [leadingCoeff_pow' hpn0', leadingCoeff_eq_zero, hpn1, one_mul, Ne, hr0, not_false_eq_true]
have hnp : 0 < natDegree p := Nat.cast_lt.1 <| by rw [← degree_eq_natDegree hp0]; exact hp
have := congr_arg natDegree hr
rw [natDegree_mul' hpnr0, natDegree_pow' hpn0', add_mul, add_assoc] at this
exact
ne_of_lt
(lt_add_of_le_of_pos (le_mul_of_one_le_right (Nat.zero_le _) hnp)
(add_pos_of_pos_of_nonneg (by rwa [one_mul]) (Nat.zero_le _)))
this⟩
