Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-11 12:23 d72119cb

View on Github →

feat(data/mv_polynomial/equiv): empty_equiv (#9122)

Estimated changes

Modified src/data/mv_polynomial/equiv.lean

added def mv_polynomial.is_empty_alg_equiv

added def mv_polynomial.is_empty_ring_equiv

deleted def mv_polynomial.pempty_alg_equiv

deleted def mv_polynomial.pempty_ring_equiv

Modified src/data/mv_polynomial/funext.lean

Modified src/ring_theory/finiteness.lean

Modified src/ring_theory/free_comm_ring.lean

Modified src/ring_theory/jacobson.lean

Modified src/ring_theory/polynomial/basic.lean