Commit 2023-02-21 08:05 e74f747c

View on Github →

feat: port LinearAlgebra.Finsupp (#2277)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Finsupp.lean

added theorem Finsupp.apply_total

added theorem Finsupp.coe_lsum

added theorem Finsupp.disjoint_lsingle_lsingle

added theorem Finsupp.disjoint_supported_supported

added theorem Finsupp.disjoint_supported_supported_iff

added theorem Finsupp.domLCongr_apply

added theorem Finsupp.domLCongr_refl

added theorem Finsupp.domLCongr_single

added theorem Finsupp.domLCongr_symm

added theorem Finsupp.domLCongr_trans

added theorem Finsupp.finsuppProdLEquiv_apply

added theorem Finsupp.finsuppProdLEquiv_symm_apply

added theorem Finsupp.fst_sumFinsuppLEquivProdFinsupp

added theorem Finsupp.infᵢ_ker_lapply_le_bot

added theorem Finsupp.ker_lsingle

added def Finsupp.lapply

added theorem Finsupp.lapply_apply

added def Finsupp.lcoeFun

added def Finsupp.lcomapDomain

added def Finsupp.lcongr

added theorem Finsupp.lcongr_apply_apply

added theorem Finsupp.lcongr_single

added theorem Finsupp.lcongr_symm

added theorem Finsupp.lcongr_symm_single

added theorem Finsupp.lhom_ext'

added theorem Finsupp.lhom_ext

added theorem Finsupp.lift_apply

added theorem Finsupp.lift_symm_apply

added def Finsupp.lmapDomain

added theorem Finsupp.lmapDomain_apply

added theorem Finsupp.lmapDomain_comp

added theorem Finsupp.lmapDomain_disjoint_ker

added theorem Finsupp.lmapDomain_id

added theorem Finsupp.lmapDomain_supported

added theorem Finsupp.lmapDomain_total

added def Finsupp.lsingle

added theorem Finsupp.lsingle_apply

added theorem Finsupp.lsingle_range_le_ker_lapply

added def Finsupp.lsubtypeDomain

added theorem Finsupp.lsubtypeDomain_apply

added def Finsupp.lsum

added theorem Finsupp.lsum_apply

added theorem Finsupp.lsum_single

added theorem Finsupp.lsum_symm_apply

added def Finsupp.mapRange.linearEquiv

added theorem Finsupp.mapRange.linearEquiv_apply

added theorem Finsupp.mapRange.linearEquiv_refl

added theorem Finsupp.mapRange.linearEquiv_symm

added theorem Finsupp.mapRange.linearEquiv_toAddEquiv

added theorem Finsupp.mapRange.linearEquiv_toLinearMap

added theorem Finsupp.mapRange.linearEquiv_trans

added def Finsupp.mapRange.linearMap

added theorem Finsupp.mapRange.linearMap_apply

added theorem Finsupp.mapRange.linearMap_comp

added theorem Finsupp.mapRange.linearMap_id

added theorem Finsupp.mapRange.linearMap_toAddMonoidHom

added theorem Finsupp.mem_span_iff_total

added theorem Finsupp.mem_span_image_iff_total

added theorem Finsupp.mem_span_range_iff_exists_finsupp

added theorem Finsupp.mem_supported'

added theorem Finsupp.mem_supported

added theorem Finsupp.mem_supported_support

added theorem Finsupp.range_restrictDom

added theorem Finsupp.range_total

added def Finsupp.restrictDom

added theorem Finsupp.restrictDom_apply

added theorem Finsupp.restrictDom_comp_subtype

added theorem Finsupp.sigmaFinsuppLEquivPiFinsupp_apply

added theorem Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply

added theorem Finsupp.single_mem_supported

added theorem Finsupp.snd_sumFinsuppLEquivProdFinsupp

added theorem Finsupp.span_eq_range_total

added theorem Finsupp.span_image_eq_map_total

added theorem Finsupp.span_single_image

added def Finsupp.sumFinsuppLEquivProdFinsupp

added theorem Finsupp.sumFinsuppLEquivProdFinsupp_symm_inl

added theorem Finsupp.sumFinsuppLEquivProdFinsupp_symm_inr

added def Finsupp.supported

added def Finsupp.supportedEquivFinsupp

added theorem Finsupp.supported_comap_lmapDomain

added theorem Finsupp.supported_empty

added theorem Finsupp.supported_eq_span_single

added theorem Finsupp.supported_inter

added theorem Finsupp.supported_interᵢ

added theorem Finsupp.supported_mono

added theorem Finsupp.supported_union

added theorem Finsupp.supported_unionᵢ

added theorem Finsupp.supported_univ

added theorem Finsupp.supᵢ_lsingle_range

added theorem Finsupp.totalOn_range

added theorem Finsupp.total_apply

added theorem Finsupp.total_apply_of_mem_supported

added theorem Finsupp.total_comapDomain

added theorem Finsupp.total_comp

added theorem Finsupp.total_comp_lmapDomain

added theorem Finsupp.total_embDomain

added theorem Finsupp.total_eq_fintype_total

added theorem Finsupp.total_eq_fintype_total_apply

added theorem Finsupp.total_equivMapDomain

added theorem Finsupp.total_fin_zero

added theorem Finsupp.total_id_surjective

added theorem Finsupp.total_mapDomain

added theorem Finsupp.total_onFinset

added theorem Finsupp.total_option

added theorem Finsupp.total_range

added theorem Finsupp.total_single

added theorem Finsupp.total_surjective

added theorem Finsupp.total_total

added theorem Finsupp.total_unique

added theorem Finsupp.total_zero

added theorem Finsupp.total_zero_apply

added theorem Fintype.range_total

added theorem Fintype.total_apply

added theorem Fintype.total_apply_single

added theorem LinearMap.leftInverse_splittingOfFinsuppSurjective

added theorem LinearMap.leftInverse_splittingOfFunOnFintypeSurjective

added theorem LinearMap.map_finsupp_total

added def LinearMap.splittingOfFinsuppSurjective

added theorem LinearMap.splittingOfFinsuppSurjective_injective

added theorem LinearMap.splittingOfFinsuppSurjective_splits

added def LinearMap.splittingOfFunOnFintypeSurjective

added theorem LinearMap.splittingOfFunOnFintypeSurjective_injective

added theorem LinearMap.splittingOfFunOnFintypeSurjective_splits

added def Module.subsingletonEquiv

added theorem Span.finsupp_total_repr

added theorem Submodule.exists_finset_of_mem_supᵢ

added theorem Submodule.mem_supᵢ_iff_exists_finset

added theorem mem_span_finset

added theorem mem_span_range_iff_exists_fun

added theorem mem_span_set

added theorem top_le_span_range_iff_forall_exists_fun