feat(algebra/module/graded_module): define graded module

[jjaassoonn]

By imitating the current graded_algebra, this pr builds graded_module over some graded algebra

Co-authored-by: Eric Wieser @eric-wieser

• [x] depends on: #14626
• [x] depends on: #15654

---

[eric-wieser]

It might make sense to handle #14583 first, so that we can avoid having extra scalar rings here.

[jjaassoonn]

There is a weird issue: if I put instances like set_like \sigma A etc inside def/lemma, then Lean can find them, but if I put them in variables, then Lean cannot find them.

[eric-wieser]

You probably need an include \sigma line to make lean aware that you intend to refer to \sigma

[jjaassoonn]

This works, thanks

You probably need an include \sigma line to make lean aware that you intend to refer to \sigma

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#14626~~
• ~~leanprover-community/mathlib#15654~~ By Dependent Issues (🤖). Happy coding!

[jjaassoonn]

@eric-wieser, this PR has been forgotten by me and you. Could you please have a look again please. Thanks.

[alreadydone]

Hmm, this merge didn't go well ... Shouldn't have squash-merged ... should be fine now.

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests