Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-15 18:15 3ec8c1d4

View on Github →

feat(algebra/direct_sum_graded): a direct_sum formed of powers of a submodule of an algebra inherits a ring structure (#6550) This also fixes some incorrect universe parameters to the of_submodules constructors.

Estimated changes

Modified src/algebra/direct_sum_graded.lean

modified def direct_sum.gcomm_monoid.of_add_subgroups

modified def direct_sum.gcomm_monoid.of_add_submonoids

modified def direct_sum.gcomm_monoid.of_submodules

modified def direct_sum.ghas_mul.of_add_subgroups

modified def direct_sum.ghas_mul.of_add_submonoids

modified def direct_sum.ghas_mul.of_submodules

modified def direct_sum.ghas_one.of_add_subgroups

modified def direct_sum.ghas_one.of_add_submonoids

modified def direct_sum.ghas_one.of_submodules

modified def direct_sum.gmonoid.of_add_subgroups

modified def direct_sum.gmonoid.of_add_submonoids

modified def direct_sum.gmonoid.of_submodules