Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-23 15:36 c78ee2be

View on Github →

feat(data/polynomial/ring_division): add roots_pow, roots_monomial (#17663)

  • Add polynomial.roots_pow, polynomial.roots_X_pow, polynomial.roots_C_mul_X_pow, and polynomial.roots_monomial.
  • Golf some proofs.

Estimated changes

deleted theorem polynomial.roots_C_mul
added theorem polynomial.roots_C_mul
added theorem polynomial.roots_X
added theorem polynomial.roots_X_pow
added theorem polynomial.roots_pow