Theorems · Theorem · field theory

Polynomial.rootMultiplicity_eq_multiplicity

∀ {R : Type u} [inst : Ring R] [inst_1 : DecidableEq R] (p : Polynomial R) (a : R),
  Polynomial.rootMultiplicity a p = if p = 0 then 0 else multiplicity (Polynomial.X - Polynomial.C a) p

Defined in

Mathlib.Algebra.Polynomial.Div

Cited by

8 results in Mathlib

Foundations

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

Assumes

RingDecidableEq