Commit 2023-03-31 10:48 c04b29dd

View on Github →

feat: port RingTheory.MvPolynomial.WeightedHomogeneous (#3192)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean

added theorem MvPolynomial.IsWeightedHomogeneous.add

added theorem MvPolynomial.IsWeightedHomogeneous.coeff_eq_zero

added theorem MvPolynomial.IsWeightedHomogeneous.inj_right

added theorem MvPolynomial.IsWeightedHomogeneous.mul

added theorem MvPolynomial.IsWeightedHomogeneous.prod

added theorem MvPolynomial.IsWeightedHomogeneous.sum

added theorem MvPolynomial.IsWeightedHomogeneous.weighted_total_degree

added def MvPolynomial.IsWeightedHomogeneous

added theorem MvPolynomial.coeff_weightedHomogeneousComponent

added theorem MvPolynomial.isWeightedHomogeneous_C

added theorem MvPolynomial.isWeightedHomogeneous_X

added theorem MvPolynomial.isWeightedHomogeneous_monomial

added theorem MvPolynomial.isWeightedHomogeneous_of_total_degree_zero

added theorem MvPolynomial.isWeightedHomogeneous_one

added theorem MvPolynomial.isWeightedHomogeneous_zero

added theorem MvPolynomial.le_weightedTotalDegree

added theorem MvPolynomial.mem_weightedHomogeneousSubmodule

added theorem MvPolynomial.sum_weightedHomogeneousComponent

added def MvPolynomial.weightedDegree'

added def MvPolynomial.weightedHomogeneousComponent

added theorem MvPolynomial.weightedHomogeneousComponent_C_mul

added theorem MvPolynomial.weightedHomogeneousComponent_apply

added theorem MvPolynomial.weightedHomogeneousComponent_eq_zero'

added theorem MvPolynomial.weightedHomogeneousComponent_eq_zero

added theorem MvPolynomial.weightedHomogeneousComponent_finsupp

added theorem MvPolynomial.weightedHomogeneousComponent_isWeightedHomogeneous

added theorem MvPolynomial.weightedHomogeneousComponent_weighted_homogeneous_polynomial

added theorem MvPolynomial.weightedHomogeneousComponent_zero

added def MvPolynomial.weightedHomogeneousSubmodule

added theorem MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported

added theorem MvPolynomial.weightedHomogeneousSubmodule_mul

added def MvPolynomial.weightedTotalDegree'

added theorem MvPolynomial.weightedTotalDegree'_eq_bot_iff

added theorem MvPolynomial.weightedTotalDegree'_zero

added def MvPolynomial.weightedTotalDegree

added theorem MvPolynomial.weightedTotalDegree_coe

added theorem MvPolynomial.weightedTotalDegree_zero