Theorem MvPolynomial.weightedHomogeneousComponent_of_isWeightedHomogeneous_same
Modification history
2025-10-06 21:14
Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
chore(RingTheory/MvPolynomial): deprecate `weightedHomogeneousComponent_of_isWeightedHomogeneous_same` and `weightedHomogeneousComponent_of_isWeightedHomogeneous_ne` (#28305)
Deleted MvPolynomial.weightedHomogeneousComponent_of_isWeightedHomogeneous_sameView on Github →