Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-03 16:11 2f44ac8f

View on Github →

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.

Estimated changes