Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-30 16:16 f7b9d6b4

View on Github →

refactor(data/equiv/algebra): mv_polynomial mv_polynomial (β ⊕ γ) α ≃r mv_polynomial β (mv_polynomial γ α)

Estimated changes

Modified src/data/equiv/algebra.lean

added theorem mv_polynomial.hom_eq_hom

added theorem mv_polynomial.is_id

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

deleted def mv_polynomial.of_option

deleted theorem mv_polynomial.of_option_C

deleted theorem mv_polynomial.of_option_X_none

deleted theorem mv_polynomial.of_option_X_some

deleted theorem mv_polynomial.of_option_add

deleted theorem mv_polynomial.of_option_mul

deleted theorem mv_polynomial.of_option_to_option

added def mv_polynomial.option_equiv_left

added def mv_polynomial.option_equiv_right

deleted def mv_polynomial.option_ring_equiv

added def mv_polynomial.punit_ring_equiv

added def mv_polynomial.rename

added theorem mv_polynomial.rename_C

added theorem mv_polynomial.rename_X

added theorem mv_polynomial.rename_id

added theorem mv_polynomial.rename_rename

added def mv_polynomial.ring_equiv_congr

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

deleted def mv_polynomial.to_option

deleted theorem mv_polynomial.to_option_C

deleted theorem mv_polynomial.to_option_C_C

deleted theorem mv_polynomial.to_option_C_X

deleted theorem mv_polynomial.to_option_X

deleted theorem mv_polynomial.to_option_add

deleted theorem mv_polynomial.to_option_mul

deleted theorem mv_polynomial.to_option_of_option

Modified src/linear_algebra/multivariate_polynomial.lean

added theorem mv_polynomial.eval₂_pow