Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-06 12:40 89431cf4

View on Github →

feat(linear_algebra): direct sum

Estimated changes

Created data/dfinsupp.lean

added def decidable_zero_symm

added theorem dfinsupp.add_apply

added theorem dfinsupp.eq_mk_support

added def dfinsupp.erase

added theorem dfinsupp.erase_add_single

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_apply_neg

added theorem dfinsupp.filter_apply_pos

added theorem dfinsupp.filter_def

added theorem dfinsupp.filter_pos_add_filter_neg

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 def dfinsupp.map_range

added theorem dfinsupp.map_range_apply

added theorem dfinsupp.map_range_def

added theorem dfinsupp.map_range_single

added theorem dfinsupp.mem_support_iff

added theorem dfinsupp.mem_support_to_fun

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 theorem dfinsupp.prod_add_index

added theorem dfinsupp.prod_finset_sum_index

added theorem dfinsupp.prod_map_range_index

added theorem dfinsupp.prod_neg_index

added theorem dfinsupp.prod_single_index

added theorem dfinsupp.prod_subtype_domain_index

added theorem dfinsupp.prod_sum_index

added theorem dfinsupp.prod_zero_index

added def dfinsupp.single

added theorem dfinsupp.single_add

added theorem dfinsupp.single_add_erase

added theorem dfinsupp.single_apply

added theorem dfinsupp.single_eq_of_ne

added theorem dfinsupp.single_eq_same

added theorem dfinsupp.single_smul

added theorem dfinsupp.single_zero

added theorem dfinsupp.smul_apply

added theorem dfinsupp.sub_apply

added def dfinsupp.subtype_domain

added theorem dfinsupp.subtype_domain_add

added theorem dfinsupp.subtype_domain_apply

added theorem dfinsupp.subtype_domain_def

added theorem dfinsupp.subtype_domain_finsupp_sum

added theorem dfinsupp.subtype_domain_neg

added theorem dfinsupp.subtype_domain_sub

added theorem dfinsupp.subtype_domain_sum

added theorem dfinsupp.subtype_domain_zero

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_eq_empty

added theorem dfinsupp.support_erase

added theorem dfinsupp.support_filter

added theorem dfinsupp.support_map_range

added theorem dfinsupp.support_mk_subset

added theorem dfinsupp.support_neg

added theorem dfinsupp.support_single_ne_zero

added theorem dfinsupp.support_single_subset

added theorem dfinsupp.support_subset_iff

added theorem dfinsupp.support_subtype_domain

added theorem dfinsupp.support_sum

added theorem dfinsupp.support_zero

added theorem dfinsupp.support_zip_with

added def dfinsupp.to_has_scalar

added def dfinsupp.to_module

added theorem dfinsupp.zero_apply

added def dfinsupp.zip_with

added theorem dfinsupp.zip_with_apply

added theorem dfinsupp.zip_with_def

added def dfinsupp

Modified data/finset.lean

added theorem multiset.to_finset_add

added theorem multiset.to_finset_zero

Created linear_algebra/direct_sum_module.lean

added def direct_sum.mk

added theorem direct_sum.mk_inj

added def direct_sum.of

added theorem direct_sum.of_inj

added def direct_sum.set_to_set

added theorem direct_sum.to_module.ext

added theorem direct_sum.to_module.of

added theorem direct_sum.to_module.unique

added def direct_sum.to_module

added theorem direct_sum.to_module_apply

added theorem direct_sum.to_module_aux.add

added theorem direct_sum.to_module_aux.smul

added def direct_sum.to_module_aux

added def direct_sum

Modified linear_algebra/tensor_product.lean

added def tensor_product.direct_sum