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
added def direct_sum.lmk
added def direct_sum.lof
deleted def direct_sum.mk
deleted theorem direct_sum.mk_inj
added theorem direct_sum.mk_smul
deleted def direct_sum.of
deleted theorem direct_sum.of_inj
added theorem direct_sum.of_smul
modified theorem direct_sum.to_module.ext
deleted theorem direct_sum.to_module.of
modified theorem direct_sum.to_module.unique
modified def direct_sum.to_module
deleted def direct_sum