mathlib

59cdeb0d - feat(algebra/module/graded_module): define graded module (#14582)

feat(algebra/module/graded_module): define graded module (#14582) 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 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>