mathlib3

3ec8c1d4 - feat(algebra/direct_sum_graded): a direct_sum formed of powers of a submodule of an algebra inherits a ring structure (#6550)