Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-15 19:37 0a6e7057

View on Github →

refactor(data/equiv/algebra): move polynomial lemmas from equiv/algebra to mv_polynomial (#731)

refactor(data/equiv/algebra): move polynomial lemma from equiv/algebra to mv_polynomial
remove update-mathlib.py

Estimated changes

Modified src/category_theory/instances/rings.lean

Modified src/data/equiv/algebra.lean

deleted def mv_polynomial.iter_to_sum

deleted theorem mv_polynomial.iter_to_sum_C_C

deleted theorem mv_polynomial.iter_to_sum_C_X

deleted theorem mv_polynomial.iter_to_sum_X

deleted def mv_polynomial.mv_polynomial_equiv_mv_polynomial

deleted def mv_polynomial.option_equiv_left

deleted def mv_polynomial.option_equiv_right

deleted def mv_polynomial.pempty_ring_equiv

deleted def mv_polynomial.punit_ring_equiv

deleted def mv_polynomial.ring_equiv_congr

deleted def mv_polynomial.ring_equiv_of_equiv

deleted def mv_polynomial.sum_ring_equiv

deleted def mv_polynomial.sum_to_iter

deleted theorem mv_polynomial.sum_to_iter_C

deleted theorem mv_polynomial.sum_to_iter_Xl

deleted theorem mv_polynomial.sum_to_iter_Xr

Modified src/linear_algebra/multivariate_polynomial.lean

added def mv_polynomial.iter_to_sum

added theorem mv_polynomial.iter_to_sum_C_C

added theorem mv_polynomial.iter_to_sum_C_X

added theorem mv_polynomial.iter_to_sum_X

added def mv_polynomial.mv_polynomial_equiv_mv_polynomial

added def mv_polynomial.option_equiv_left

added def mv_polynomial.option_equiv_right

added def mv_polynomial.pempty_ring_equiv

added def mv_polynomial.punit_ring_equiv

added def mv_polynomial.ring_equiv_congr

added def mv_polynomial.ring_equiv_of_equiv

added def mv_polynomial.sum_ring_equiv

added def mv_polynomial.sum_to_iter

added theorem mv_polynomial.sum_to_iter_C

added theorem mv_polynomial.sum_to_iter_Xl

added theorem mv_polynomial.sum_to_iter_Xr

Modified src/ring_theory/noetherian.lean