Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mv_polynomial.of_option_C

Modification history

2019-01-30 16:16
src/data/equiv/algebra.lean
refactor(data/equiv/algebra): mv_polynomial mv_polynomial (β ⊕ γ) α ≃r mv_polynomial β (mv_polynomial γ α)
Deleted mv_polynomial.of_option_CView on Github →
2019-01-29 17:15
src/data/equiv/algebra.lean
feat(data/equiv/algebra): ring equiv for mv_polynomial
Added mv_polynomial.of_option_CView on Github →