feat(algebra/free_algebra): Define a grading

Open eric-wieser opened this issue 5 years ago • 3 comments

The grading takes the form free_algebra R X →ₐ[R] add_monoid_algebra (free_algebra R X) ℕ

It's likely that there are more generic lemmas about grading that can be shared with tensor_algebra and friends, but that's left to follow-up work

[x] depends on #4315 (first commit)
[x] depends on #4365
[x] depends on #4603
[x] depends on #4789

Sep 29 '20 14:09 eric-wieser

Is the base of this PR supposed to be the branch for #4315 or should it be master?

Oct 12 '20 15:10 bryangingechen

The base is set up this way just to make the diff look reasonable. I suppose at this point the base branch has only two lines difference from master, so I may as well switch it back.

Oct 12 '20 15:10 eric-wieser

Now without any real changes to add_monoid_algebra, since those were split to other PRs.

Oct 28 '20 22:10 eric-wieser