Commit 2020-09-14 09:42 bbfeff38

View on Github →

feat(data/mv_polynomial/monad): mv_polynomial is a monad in two different ways (#4080) These definitions and lemmas significantly decrease the pain in several computations in the Witt project.

Estimated changes

Created src/data/mv_polynomial/monad.lean

added theorem mv_polynomial.aeval_X_left

added theorem mv_polynomial.aeval_X_left_apply

added theorem mv_polynomial.aeval_bind₁

added theorem mv_polynomial.aeval_bind₂

added theorem mv_polynomial.aeval_comp_bind₁

added theorem mv_polynomial.aeval_eq_bind₁

added theorem mv_polynomial.aeval_id_eq_join₁

added theorem mv_polynomial.aeval_rename

added def mv_polynomial.bind₁

added theorem mv_polynomial.bind₁_C_right

added theorem mv_polynomial.bind₁_X_left

added theorem mv_polynomial.bind₁_X_right

added theorem mv_polynomial.bind₁_bind₁

added theorem mv_polynomial.bind₁_comp_bind₁

added theorem mv_polynomial.bind₁_id

added theorem mv_polynomial.bind₁_monomial

added theorem mv_polynomial.bind₁_rename

added def mv_polynomial.bind₂

added theorem mv_polynomial.bind₂_C_left

added theorem mv_polynomial.bind₂_C_right

added theorem mv_polynomial.bind₂_X_right

added theorem mv_polynomial.bind₂_bind₂

added theorem mv_polynomial.bind₂_comp_C

added theorem mv_polynomial.bind₂_comp_bind₂

added theorem mv_polynomial.bind₂_id

added theorem mv_polynomial.bind₂_map

added theorem mv_polynomial.bind₂_monomial

added theorem mv_polynomial.bind₂_monomial_one

added theorem mv_polynomial.eval₂_hom_C_eq_bind₁

added theorem mv_polynomial.eval₂_hom_C_id_eq_join₁

added theorem mv_polynomial.eval₂_hom_C_left

added theorem mv_polynomial.eval₂_hom_bind₁

added theorem mv_polynomial.eval₂_hom_bind₂

added theorem mv_polynomial.eval₂_hom_comp_C

added theorem mv_polynomial.eval₂_hom_comp_bind₂

added theorem mv_polynomial.eval₂_hom_eq_bind₂

added theorem mv_polynomial.eval₂_hom_id_X_eq_join₂

added theorem mv_polynomial.hom_bind₁

added def mv_polynomial.join₁

added theorem mv_polynomial.join₁_rename

added def mv_polynomial.join₂

added theorem mv_polynomial.join₂_comp_map

added theorem mv_polynomial.join₂_map

added theorem mv_polynomial.map_bind₁

added theorem mv_polynomial.map_bind₂

added theorem mv_polynomial.map_comp_C

added theorem mv_polynomial.rename_bind₁