mathlib3

f7795d1a - feat(monoid_algebra/grading): `add_monoid_algebra`s permit an internal grading (#8927)