Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-23 22:12 4ec88dbe

View on Github →

feat(algebra/direct_sum): Bundle the homomorphisms (#4754)

Estimated changes

modified def direct_sum.mk
deleted theorem direct_sum.mk_add
deleted theorem direct_sum.mk_neg
deleted theorem direct_sum.mk_sub
deleted theorem direct_sum.mk_zero
modified def direct_sum.of
deleted theorem direct_sum.of_add
deleted theorem direct_sum.of_neg
deleted theorem direct_sum.of_sub
deleted theorem direct_sum.of_zero
modified def direct_sum.to_group
deleted theorem direct_sum.to_group_add
deleted theorem direct_sum.to_group_neg
deleted theorem direct_sum.to_group_sub
deleted theorem direct_sum.to_group_zero