one_lt_rootMultiplicity_iff_isRoot_gcd

English

In a gcd-friendly setting, 1 < rootMultiplicity t p is equivalent to gcd(p, p') having a root at t.

Русский

В условиях, подходящих для НОГД, 1 < кратность корня p в t эквивалентна тому, что НОД(p, p') имеет корень в t.

LaTeX

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

Lean4

theorem one_lt_rootMultiplicity_iff_isRoot_gcd [GCDMonoid R[X]] {p : R[X]} {t : R} (h : p ≠ 0) :
    1 < p.rootMultiplicity t ↔ (gcd p (derivative p)).IsRoot t := by
  simp_rw [one_lt_rootMultiplicity_iff_isRoot h, ← dvd_iff_isRoot, dvd_gcd_iff]

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