Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-25 22:55 56de12a7

View on Github →

refactor(data/mv_polynomial): upgrade monomial to a linear_map (#9870)

Estimated changes

Modified src/data/mv_polynomial/basic.lean

added theorem mv_polynomial.C_eq_smul_one

added theorem mv_polynomial.X_pow_eq_monomial

deleted theorem mv_polynomial.X_pow_eq_single

added theorem mv_polynomial.eval₂_mul_C

added theorem mv_polynomial.finsupp_support_eq_support

modified def mv_polynomial.monomial

deleted theorem mv_polynomial.monomial_add

added theorem mv_polynomial.monomial_finsupp_sum_index

added def mv_polynomial.monomial_one_hom

added theorem mv_polynomial.monomial_one_hom_apply

added theorem mv_polynomial.monomial_pow

added theorem mv_polynomial.monomial_sum_index

added theorem mv_polynomial.monomial_sum_one

added theorem mv_polynomial.monomial_zero'

modified theorem mv_polynomial.sum_monomial_eq

Modified src/data/mv_polynomial/comm_ring.lean

deleted theorem mv_polynomial.monomial_neg

deleted theorem mv_polynomial.monomial_sub

Modified src/data/mv_polynomial/monad.lean

Modified src/data/mv_polynomial/pderiv.lean

Modified src/data/mv_polynomial/rename.lean

Modified src/ring_theory/mv_polynomial/basic.lean

Modified src/ring_theory/polynomial/symmetric.lean

Modified src/ring_theory/witt_vector/witt_polynomial.lean