Commit 2023-04-07 15:02 5a04e704

View on Github →

feat: port RingTheory.MvPolynomial.Basic (#3329)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/MvPolynomial/Basic.lean

added def MvPolynomial.basisMonomials

added theorem MvPolynomial.coe_basisMonomials

added theorem MvPolynomial.linearIndependent_X

added theorem MvPolynomial.mapRange_eq_map

added theorem MvPolynomial.mem_restrictDegree

added theorem MvPolynomial.mem_restrictDegree_iff_sup

added theorem MvPolynomial.mem_restrictTotalDegree

added def MvPolynomial.restrictDegree

added def MvPolynomial.restrictTotalDegree

added theorem Polynomial.coe_basisMonomials