Commit 2023-04-04 12:51 4b272b5d

View on Github →

feat: port Data.MvPolynomial.Expand (#3261)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/MvPolynomial/Expand.lean

added theorem MvPolynomial.expand_C

added theorem MvPolynomial.expand_X

added theorem MvPolynomial.expand_bind₁

added theorem MvPolynomial.expand_comp_bind₁

added theorem MvPolynomial.expand_monomial

added theorem MvPolynomial.expand_one

added theorem MvPolynomial.expand_one_apply

added theorem MvPolynomial.map_expand

added theorem MvPolynomial.rename_comp_expand

added theorem MvPolynomial.rename_expand