Theorems · Theorem · field theory

Polynomial.rootMultiplicity_eq_nat_find_of_nonzero

Deprecated since 2026-02-12Use Polynomial.rootMultiplicity_eq_natFind_of_ne_zero instead.

∀ {R : Type u} [inst : Ring R] {p : Polynomial R} (p0 : p ≠ 0) {a : R}
  [inst_1 : DecidablePred fun n => ¬(Polynomial.X - Polynomial.C a) ^ (n + 1) ∣ p],
  Polynomial.rootMultiplicity a p = Nat.find ⋯

Alias of Polynomial.rootMultiplicity_eq_natFind_of_ne_zero.

Defined in

Mathlib.Algebra.Polynomial.Div

Cited by

0 results in Mathlib

Foundations

Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingDecidablePred