Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-28 10:14 afa31bed

View on Github →

refactor(linear_algebra/direct_sum_module): move to algebra/direct_sum

Estimated changes

added def direct_sum.mk
added theorem direct_sum.mk_add
added theorem direct_sum.mk_inj
added theorem direct_sum.mk_neg
added theorem direct_sum.mk_sub
added theorem direct_sum.mk_zero
added def direct_sum.of
added theorem direct_sum.of_add
added theorem direct_sum.of_inj
added theorem direct_sum.of_neg
added theorem direct_sum.of_sub
added theorem direct_sum.of_zero
added theorem direct_sum.to_group_of
added def direct_sum