Def add_monoid_algebra.decompose_aux

Modification history

2022-04-21 12:09

src/algebra/monoid_algebra/grading.lean

feat(algebra/monoid_algebra/grading): Use the new graded_algebra API (#13360) …

Added add_monoid_algebra.decompose_aux View on Github →