mathlib3

761801fd - feat(algebra/monoid_algebra/grading): Use the new graded_algebra API (#13360)

feat(algebra/monoid_algebra/grading): Use the new graded_algebra API (#13360) This removes `to_grades_by` and `of_grades_by`, and prefers `graded_algebra.decompose` as the canonical spelling. This might undo some of the performance improvements in #13169, but it's not clear where to apply the analogous changes here, or whether they're really needed any more anyway,