le_rootMultiplicity_iff — Mathlib

English

For any p, p.rootMultiplicity 0 equals p.natTrailingDegree.

Русский

Для любого p, p.rootMultiplicity 0 равна p.natTrailingDegree.

LaTeX

$$$ p.rootMultiplicity\,0 = p.natTrailingDegree $$$

Lean4

/-- The multiplicity of `a` as root of a nonzero polynomial `p` is at least `n` iff
`(X - a) ^ n` divides `p`. -/
theorem le_rootMultiplicity_iff (p0 : p ≠ 0) {a : R} {n : ℕ} : n ≤ rootMultiplicity a p ↔ (X - C a) ^ n ∣ p := by
  classical
  simp_rw [rootMultiplicity_eq_nat_find_of_nonzero p0, @Nat.le_find_iff _ (_), Classical.not_not]
  refine ⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩
  rcases n with - | n
  · rw [pow_zero]
    apply one_dvd
  · exact h n n.lt_succ_self

Похожие утверждения