Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-29 18:26 d709ed6f

View on Github →

feat(algebra/direct_sum*): relax a lot of constraints to add_comm_monoid (#3537)

Estimated changes

Modified src/algebra/direct_limit.lean

Modified src/algebra/direct_sum.lean

added theorem direct_sum.sub_apply

added theorem direct_sum.to_add_monoid.unique

added def direct_sum.to_add_monoid

added theorem direct_sum.to_add_monoid_of

deleted theorem direct_sum.to_group.unique

deleted def direct_sum.to_group

deleted theorem direct_sum.to_group_of

modified def direct_sum

Modified src/linear_algebra/direct_sum_module.lean

modified theorem direct_sum.smul_apply