Mathlib Changelog
v3
Changelog
About
Github
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
src/algebra/direct_sum.lean
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
Modified
src/linear_algebra/direct_sum/finsupp.lean
Modified
src/linear_algebra/direct_sum_module.lean