Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-13 22:15 6f401acf

View on Github →

feat(data/polynomial/*): suggestions from the generalization linter (#13342)

Estimated changes

Modified src/data/complex/exponential.lean

modified theorem is_cau_geo_series

Modified src/data/polynomial/algebra_map.lean

modified theorem polynomial.eval₂_algebra_map_X

Modified src/data/polynomial/cancel_leads.lean

Modified src/data/polynomial/degree/definitions.lean

added theorem polynomial.sum_fin

Modified src/data/polynomial/derivative.lean

Modified src/data/polynomial/div.lean

deleted theorem polynomial.sum_fin

Modified src/data/polynomial/eval.lean

modified theorem polynomial.support_map_subset

Modified src/data/polynomial/field_division.lean

modified theorem polynomial.degree_map

modified theorem polynomial.leading_coeff_map

modified theorem polynomial.monic_map_iff

modified theorem polynomial.nat_degree_map

Modified src/data/polynomial/integral_normalization.lean

Modified src/data/polynomial/monic.lean

Modified src/data/polynomial/reverse.lean

modified theorem polynomial.reverse_mul_of_domain

modified theorem polynomial.trailing_coeff_mul

Modified src/data/polynomial/ring_division.lean