Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-16 12:38 f7430cd7

View on Github →

feat(data/polynomial/eval): add protected on some lemmas about polynomial.map (#13478) These clash with global lemmas.

Estimated changes

Modified src/algebra/polynomial/group_ring_action.lean

Modified src/data/polynomial/derivative.lean

Modified src/data/polynomial/div.lean

Modified src/data/polynomial/eval.lean

deleted theorem polynomial.map_add

deleted theorem polynomial.map_mul

deleted theorem polynomial.map_neg

deleted theorem polynomial.map_one

deleted theorem polynomial.map_sub

deleted theorem polynomial.map_zero

Modified src/data/polynomial/field_division.lean

Modified src/data/polynomial/lifts.lean

Modified src/data/polynomial/ring_division.lean

Modified src/field_theory/polynomial_galois_group.lean

Modified src/field_theory/separable.lean

Modified src/field_theory/splitting_field.lean

Modified src/ring_theory/eisenstein_criterion.lean

Modified src/ring_theory/polynomial/cyclotomic/basic.lean

Modified src/ring_theory/polynomial/dickson.lean

Modified src/ring_theory/polynomial/gauss_lemma.lean