Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-24 22:06 e66e136f

View on Github →

feat(data/mv_polynomial/basic): add two equivs (#6324) Two small lemma about mv_polynomial as R-algebra.

Estimated changes

Modified src/data/mv_polynomial/equiv.lean

added def mv_polynomial.alg_equiv_congr

added def mv_polynomial.alg_equiv_congr_left

added def mv_polynomial.alg_equiv_congr_right

deleted def mv_polynomial.alg_equiv_of_equiv

added def mv_polynomial.sum_alg_equiv

Modified src/ring_theory/finiteness.lean