Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-15 07:04 249fd4f2

View on Github →

refactor(data/polynomial,ring_theory): use big operators for polynomials (#6616) This untangles some more definitions on polynomials from finsupp. This uses the same approach as in #6605.

Estimated changes

Modified src/data/polynomial/div.lean

added theorem polynomial.coeff_div_X

Modified src/data/polynomial/integral_normalization.lean

modified theorem polynomial.integral_normalization_aeval_eq_zero

added theorem polynomial.integral_normalization_coeff

modified theorem polynomial.integral_normalization_eval₂_eq_zero

added theorem polynomial.integral_normalization_support

added theorem polynomial.integral_normalization_zero

modified theorem polynomial.support_integral_normalization

Modified src/ring_theory/algebraic.lean

Modified src/ring_theory/polynomial/rational_root.lean

Modified src/ring_theory/polynomial/scale_roots.lean