Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-28 01:10 7d4d985b

View on Github →

chore(data/polynomial): make eval2 irreducible (#3543) A while back @gebner identified that an unfortunate timeout could be avoided by making polynomial.eval2 irreducible. This PR does that. It's not perfect: on a few occasions I have to temporarily set it back to semireducible, because it looks like the proofs really do some heavy refling. I'd like to make more things irreducible in the polynomial API, but not yet.

Estimated changes

Modified src/data/polynomial/algebra_map.lean

Modified src/data/polynomial/degree.lean

Modified src/data/polynomial/eval.lean

added theorem polynomial.comp_eq_sum_left

added theorem polynomial.eval_eq_sum

added theorem polynomial.eval₂_eq_sum

Modified src/data/polynomial/identities.lean

Modified src/field_theory/fixed.lean

Modified src/field_theory/minimal_polynomial.lean

Modified src/field_theory/separable.lean

added theorem polynomial.expand_eq_sum

Modified src/ring_theory/algebra.lean

added theorem algebra.subring_algebra_map_apply

added theorem algebra.subring_coe_algebra_map

added theorem algebra.subring_coe_algebra_map_hom

Modified src/ring_theory/integral_closure.lean

modified theorem integral_closure_idem

added theorem is_integral_of_is_algebra_tower

Modified src/ring_theory/polynomial/basic.lean

added theorem polynomial.map_restriction

Modified src/ring_theory/polynomial/rational_root.lean

Modified src/topology/algebra/polynomial.lean