Commit 2023-04-04 01:03 3ec9411a

View on Github →

feat: port Data.MvPolynomial.Monad (#2887)

depends on: #2861
depends on: #2886

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/MvPolynomial/Monad.lean

added theorem MvPolynomial.aeval_bind₁

added theorem MvPolynomial.aeval_bind₂

added theorem MvPolynomial.aeval_comp_bind₁

added theorem MvPolynomial.aeval_eq_bind₁

added theorem MvPolynomial.aeval_id_eq_join₁

added theorem MvPolynomial.aeval_id_rename

added def MvPolynomial.bind₁

added theorem MvPolynomial.bind₁_C_right

added theorem MvPolynomial.bind₁_X_left

added theorem MvPolynomial.bind₁_X_right

added theorem MvPolynomial.bind₁_bind₁

added theorem MvPolynomial.bind₁_comp_bind₁

added theorem MvPolynomial.bind₁_comp_rename

added theorem MvPolynomial.bind₁_id

added theorem MvPolynomial.bind₁_monomial

added theorem MvPolynomial.bind₁_rename

added def MvPolynomial.bind₂

added theorem MvPolynomial.bind₂_C_left

added theorem MvPolynomial.bind₂_C_right

added theorem MvPolynomial.bind₂_X_right

added theorem MvPolynomial.bind₂_bind₂

added theorem MvPolynomial.bind₂_comp_C

added theorem MvPolynomial.bind₂_comp_bind₂

added theorem MvPolynomial.bind₂_id

added theorem MvPolynomial.bind₂_map

added theorem MvPolynomial.bind₂_monomial

added theorem MvPolynomial.bind₂_monomial_one

added theorem MvPolynomial.eval₂Hom_C_eq_bind₁

added theorem MvPolynomial.eval₂Hom_C_id_eq_join₁

added theorem MvPolynomial.eval₂Hom_C_left

added theorem MvPolynomial.eval₂Hom_bind₁

added theorem MvPolynomial.eval₂Hom_bind₂

added theorem MvPolynomial.eval₂Hom_comp_C

added theorem MvPolynomial.eval₂Hom_comp_bind₂

added theorem MvPolynomial.eval₂Hom_eq_bind₂

added theorem MvPolynomial.eval₂Hom_id_X_eq_join₂

added theorem MvPolynomial.hom_bind₁

added def MvPolynomial.join₁

added theorem MvPolynomial.join₁_rename

added def MvPolynomial.join₂

added theorem MvPolynomial.join₂_comp_map

added theorem MvPolynomial.join₂_map

added theorem MvPolynomial.map_bind₁

added theorem MvPolynomial.map_bind₂

added theorem MvPolynomial.map_comp_C

added theorem MvPolynomial.mem_vars_bind₁

added theorem MvPolynomial.rename_bind₁

added theorem MvPolynomial.rename_comp_bind₁

added theorem MvPolynomial.vars_bind₁