Commit 2023-05-20 10:39 74203d92

View on Github →

feat: port RingTheory.MvPolynomial.Homogeneous (#4138)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

added theorem MvPolynomial.IsHomogeneous.add

added theorem MvPolynomial.IsHomogeneous.coeff_eq_zero

added theorem MvPolynomial.IsHomogeneous.inj_right

added theorem MvPolynomial.IsHomogeneous.mul

added theorem MvPolynomial.IsHomogeneous.prod

added theorem MvPolynomial.IsHomogeneous.sum

added theorem MvPolynomial.IsHomogeneous.totalDegree

added def MvPolynomial.IsHomogeneous

added theorem MvPolynomial.coeff_homogeneousComponent

added def MvPolynomial.homogeneousComponent

added theorem MvPolynomial.homogeneousComponent_C_mul

added theorem MvPolynomial.homogeneousComponent_apply

added theorem MvPolynomial.homogeneousComponent_eq_zero'

added theorem MvPolynomial.homogeneousComponent_eq_zero

added theorem MvPolynomial.homogeneousComponent_homogeneous_polynomial

added theorem MvPolynomial.homogeneousComponent_isHomogeneous

added theorem MvPolynomial.homogeneousComponent_zero

added def MvPolynomial.homogeneousSubmodule

added theorem MvPolynomial.homogeneousSubmodule_eq_finsupp_supported

added theorem MvPolynomial.homogeneousSubmodule_mul

added theorem MvPolynomial.isHomogeneous_C

added theorem MvPolynomial.isHomogeneous_X

added theorem MvPolynomial.isHomogeneous_monomial

added theorem MvPolynomial.isHomogeneous_of_totalDegree_zero

added theorem MvPolynomial.isHomogeneous_one

added theorem MvPolynomial.isHomogeneous_zero

added theorem MvPolynomial.mem_homogeneousSubmodule

added theorem MvPolynomial.sum_homogeneousComponent