Mathlib Changelog
Changelog
About
Github
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