Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-21 12:09 761801fd

View on Github →

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,

Estimated changes