Theorems · Theorem · field theory

Polynomial.rootMultiplicity_eq_natFind_of_ne_zero

∀ {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 ⋯

Defined in

Mathlib.Algebra.Polynomial.Div

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingDecidablePred