Mathlib Changelog
Changelog
About
Github
Commit
2019-01-28 10:14
afa31bed
View on Github →
refactor(linear_algebra/direct_sum_module): move to algebra/direct_sum
Estimated changes
Created
src/algebra/direct_sum.lean
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
def
direct_sum.set_to_set
added
theorem
direct_sum.to_group.unique
added
def
direct_sum.to_group
added
theorem
direct_sum.to_group_add
added
theorem
direct_sum.to_group_neg
added
theorem
direct_sum.to_group_of
added
theorem
direct_sum.to_group_sub
added
theorem
direct_sum.to_group_zero
added
def
direct_sum
Modified
src/linear_algebra/direct_sum_module.lean
added
def
direct_sum.lmk
added
def
direct_sum.lof
added
def
direct_sum.lset_to_set
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
deleted
def
direct_sum.set_to_set
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
theorem
direct_sum.to_module_apply
deleted
theorem
direct_sum.to_module_aux.add
deleted
theorem
direct_sum.to_module_aux.smul
deleted
def
direct_sum.to_module_aux
added
theorem
direct_sum.to_module_lof
deleted
def
direct_sum
Modified
src/linear_algebra/tensor_product.lean
modified
def
tensor_product.direct_sum