Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-21 16:25 c47d1d0d

View on Github →

feat(data/{mv_}polynomial): make args to aeval implicit (#3494)

Estimated changes

Modified src/data/mv_polynomial.lean

modified theorem mv_polynomial.aeval_C

modified theorem mv_polynomial.aeval_X

modified theorem mv_polynomial.aeval_def

Modified src/data/polynomial/algebra_map.lean

modified theorem polynomial.aeval_C

modified theorem polynomial.aeval_X

modified theorem polynomial.aeval_alg_hom

modified theorem polynomial.aeval_alg_hom_apply

modified theorem polynomial.aeval_def

modified theorem polynomial.coeff_zero_eq_aeval_zero

Modified src/data/polynomial/monic.lean

Modified src/data/polynomial/ring_division.lean

Modified src/field_theory/minimal_polynomial.lean

modified theorem minimal_polynomial.aeval

modified theorem minimal_polynomial.dvd

modified theorem minimal_polynomial.min

modified theorem minimal_polynomial.unique

Modified src/ring_theory/adjoin.lean

modified theorem algebra.adjoin_singleton_eq_range

Modified src/ring_theory/adjoin_root.lean

modified theorem adjoin_root.aeval_eq

Modified src/ring_theory/algebra_tower.lean

modified theorem is_algebra_tower.aeval_apply

Modified src/ring_theory/algebraic.lean

Modified src/ring_theory/integral_closure.lean

modified theorem is_integral_trans_aux

Modified src/ring_theory/localization.lean

Modified src/ring_theory/polynomial/rational_root.lean

modified theorem denom_dvd_of_is_root

modified theorem is_integer_of_is_root_of_monic

modified theorem num_dvd_of_is_root