Commit 2024-04-15 15:25 bec5207f

View on Github →

refactor(RingTheory.MvPolynomial.Homogeneous): refactor in terms of weightedHomogeneous (#7609) We rewrite the definition of homogeneous polynomial as a special case of weighted homogeneous polynomial. Question: should all uses of ∑ i in d.support, d i be replaced by degree d?

Estimated changes

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

modified theorem MvPolynomial.IsHomogeneous.coeff_eq_zero

added def MvPolynomial.degree

modified theorem MvPolynomial.homogeneousComponent_isHomogeneous

modified theorem MvPolynomial.homogeneousComponent_zero

modified def MvPolynomial.homogeneousSubmodule

modified theorem MvPolynomial.isHomogeneous_monomial

deleted theorem MvPolynomial.isHomogeneous_of_totalDegree_zero

added theorem MvPolynomial.totalDegree_zero_iff_isHomogeneous

added theorem MvPolynomial.weightedDegree_one

added theorem MvPolynomial.weightedHomogeneousSubmodule_one

added theorem MvPolynomial.weightedTotalDegree_one

Modified Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean

added theorem MvPolynomial.IsWeightedHomogeneous.weightedHomogeneousComponent_ne

added theorem MvPolynomial.IsWeightedHomogeneous.weightedHomogeneousComponent_same

added def MvPolynomial.NonTorsionWeight

added theorem MvPolynomial.finsum_weightedHomogeneousComponent

added theorem MvPolynomial.isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero

added theorem MvPolynomial.nonTorsionWeight_of

deleted def MvPolynomial.weightedDegree'

added def MvPolynomial.weightedDegree

added theorem MvPolynomial.weightedDegree_apply

added theorem MvPolynomial.weightedDegree_eq_zero_iff

added theorem MvPolynomial.weightedHomogeneousComponent_mem

added theorem MvPolynomial.weightedTotalDegree_eq_zero_iff