Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-29 17:15 7cfcce3d

View on Github →

feat(data/equiv/algebra): ring equiv for mv_polynomial

Estimated changes

Modified src/data/equiv/algebra.lean

added def mv_polynomial.of_option

added theorem mv_polynomial.of_option_C

added theorem mv_polynomial.of_option_X_none

added theorem mv_polynomial.of_option_X_some

added theorem mv_polynomial.of_option_add

added theorem mv_polynomial.of_option_mul

added theorem mv_polynomial.of_option_to_option

added def mv_polynomial.option_ring_equiv

added def mv_polynomial.pempty_ring_equiv

added def mv_polynomial.ring_equiv_of_equiv

added def mv_polynomial.to_option

added theorem mv_polynomial.to_option_C

added theorem mv_polynomial.to_option_C_C

added theorem mv_polynomial.to_option_C_X

added theorem mv_polynomial.to_option_X

added theorem mv_polynomial.to_option_add

added theorem mv_polynomial.to_option_mul

added theorem mv_polynomial.to_option_of_option