mathlib

2f44ac8f - feat(algebra/monoid_algebra/grading): internal graded structure for an arbitrary degree function (#10435)

feat(algebra/monoid_algebra/grading): internal graded structure for an arbitrary degree function (#10435) This gives an internal graded structure of an additive monoid algebra for the grading given by an arbitrary degree function. The grading in the original file is redefined as the grading for the identity degree function.