Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-22 04:34 79bc6ad4

View on Github →

feat(data/mv_polynomial/equiv): API for mv_polynomial.fin_succ_equiv (#10812) This PR provides API for mv_polynomial.fin_succ_equiv: coefficients, degree, coefficientes of coefficients, degree_of of coefficients, etc. To state and prove these lemmas I had to define cons and tail for maps fin (n+1) →₀ M and prove the usual properties for these. I'm not sure if this is necessary or the correct approach to do this.

Estimated changes

Created src/data/finsupp/fin.lean

added def finsupp.cons

added theorem finsupp.cons_ne_zero_iff

added theorem finsupp.cons_ne_zero_of_left

added theorem finsupp.cons_ne_zero_of_right

added theorem finsupp.cons_succ

added theorem finsupp.cons_tail

added theorem finsupp.cons_zero

added theorem finsupp.cons_zero_zero

added def finsupp.tail

added theorem finsupp.tail_apply

added theorem finsupp.tail_cons

Modified src/data/mv_polynomial/equiv.lean

added theorem mv_polynomial.coeff_eval_eq_eval_coeff

added theorem mv_polynomial.degree_fin_succ_equiv

added theorem mv_polynomial.degree_of_coeff_fin_succ_equiv

added theorem mv_polynomial.eval_eq_eval_mv_eval'

modified def mv_polynomial.fin_succ_equiv

added theorem mv_polynomial.fin_succ_equiv_X_succ

added theorem mv_polynomial.fin_succ_equiv_X_zero

modified theorem mv_polynomial.fin_succ_equiv_apply

added theorem mv_polynomial.fin_succ_equiv_coeff_coeff

modified theorem mv_polynomial.fin_succ_equiv_eq

added theorem mv_polynomial.fin_succ_equiv_support'

added theorem mv_polynomial.fin_succ_equiv_support

added theorem mv_polynomial.nat_degree_fin_succ_equiv

added theorem mv_polynomial.support_coeff_fin_succ_equiv

added theorem mv_polynomial.support_fin_succ_equiv_nonempty