Commit 2018-11-06 12:40 89431cf4

View on Github →

feat(linear_algebra): direct sum

Estimated changes

added theorem dfinsupp.add_apply
added theorem dfinsupp.eq_mk_support
added def dfinsupp.erase
added theorem dfinsupp.erase_apply
added theorem dfinsupp.erase_def
added theorem dfinsupp.erase_ne
added theorem dfinsupp.erase_same
added theorem dfinsupp.ext
added def dfinsupp.filter
added theorem dfinsupp.filter_apply
added theorem dfinsupp.filter_def
added theorem dfinsupp.finite_supp
added theorem dfinsupp.induction₂
added def dfinsupp.lmk
added theorem dfinsupp.lmk_apply
added def dfinsupp.lsingle
added theorem dfinsupp.lsingle_apply
added theorem dfinsupp.map_range_def
added def dfinsupp.mk
added theorem dfinsupp.mk_add
added theorem dfinsupp.mk_apply
added theorem dfinsupp.mk_inj
added theorem dfinsupp.mk_neg
added theorem dfinsupp.mk_smul
added theorem dfinsupp.mk_sub
added theorem dfinsupp.mk_zero
added theorem dfinsupp.neg_apply
added structure dfinsupp.pre
added def dfinsupp.prod
added def dfinsupp.single
added theorem dfinsupp.single_add
added theorem dfinsupp.single_apply
added theorem dfinsupp.single_smul
added theorem dfinsupp.single_zero
added theorem dfinsupp.smul_apply
added theorem dfinsupp.sub_apply
added def dfinsupp.sum
added theorem dfinsupp.sum_add
added theorem dfinsupp.sum_apply
added theorem dfinsupp.sum_neg
added theorem dfinsupp.sum_single
added theorem dfinsupp.sum_sub_index
added theorem dfinsupp.sum_zero
added def dfinsupp.support
added theorem dfinsupp.support_add
added theorem dfinsupp.support_erase
added theorem dfinsupp.support_neg
added theorem dfinsupp.support_sum
added theorem dfinsupp.support_zero
added theorem dfinsupp.zero_apply
added theorem dfinsupp.zip_with_def
added def dfinsupp