PR !4#8788: feat(Algebra/Module/GradeZeroModule): if `A` ...

Stream: triage

[Random Issue Bot]

Today I chose PR #8788 for discussion!

feat(Algebra/Module/GradeZeroModule): if A is a graded semiring and M is a graded A-module, then each grade of M is a module over the 0-th grade of A.
Created by @None (@FMLJohn) on 2023-12-02
Labels: merge-conflict, t-algebra

Is this PR still relevant? Any recent updates? Anyone making progress?