one_lt_rootMultiplicity_iff_isRoot

English

1 < root multiplicity of p at t is equivalent to p having a root at t and the derivative having a root at t.

Русский

1 < кратность корня p в t эквивалентно тому, что p имеет корень в t и производная имеет корень в t.

LaTeX

$$$$1 < p.rootMultiplicity t \iff p.IsRoot t \land (\mathrm{derivative}\, p).IsRoot t$$$$

Lean4

theorem one_lt_rootMultiplicity_iff_isRoot {p : R[X]} {t : R} (h : p ≠ 0) :
    1 < p.rootMultiplicity t ↔ p.IsRoot t ∧ (derivative p).IsRoot t :=
  by
  rw [one_lt_rootMultiplicity_iff_isRoot_iterate_derivative h]
  refine ⟨fun h ↦ ⟨h 0 (by simp), h 1 (by simp)⟩, fun ⟨h0, h1⟩ m hm ↦ ?_⟩
  obtain (_ | _ | m) := m
  exacts [h0, h1, by cutsat]

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