Commit 2025-10-06 21:14 e9a78878
View on Github →chore(RingTheory/MvPolynomial): deprecate weightedHomogeneousComponent_of_isWeightedHomogeneous_same and weightedHomogeneousComponent_of_isWeightedHomogeneous_ne (#28305)
chore(RingTheory/MvPolynomial): deprecate weightedHomogeneousComponent_of_isWeightedHomogeneous_same and weightedHomogeneousComponent_of_isWeightedHomogeneous_ne (#28305)