rootMultiplicity_eq_natTrailingDegree'

English

For p ≠ 0 and a ∈ R, (X − a)^{rootMultiplicity a p + 1} ∤ p.

Русский

Для p ≠ 0 и a ∈ R, (X − a)^{rootMultiplicity a p + 1} не делит p.

LaTeX

$$$ \neg (X - C a)^{\operatorname{rootMultiplicity}(a,p) + 1} \nmid p $$$

Lean4

/-- See `Polynomial.rootMultiplicity_eq_natTrailingDegree` for the general case. -/
theorem rootMultiplicity_eq_natTrailingDegree' : p.rootMultiplicity 0 = p.natTrailingDegree :=
  by
  by_cases h : p = 0
  · simp only [h, rootMultiplicity_zero, natTrailingDegree_zero]
  refine le_antisymm ?_ ?_
  · rw [rootMultiplicity_le_iff h, map_zero, sub_zero, X_pow_dvd_iff, not_forall]
    exact ⟨p.natTrailingDegree, fun h' ↦ trailingCoeff_nonzero_iff_nonzero.2 h <| h' <| Nat.lt.base _⟩
  · rw [le_rootMultiplicity_iff h, map_zero, sub_zero, X_pow_dvd_iff]
    exact fun _ ↦ coeff_eq_zero_of_lt_natTrailingDegree

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