Commit 2023-03-02 20:36 88902554

View on Github →

feat: port LinearAlgebra.Dfinsupp (#2550)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Dfinsupp/Basic.lean

Created Mathlib/LinearAlgebra/Dfinsupp.lean

added theorem CompleteLattice.Independent.dfinsupp_lsum_injective

added theorem CompleteLattice.Independent.dfinsupp_sumAddHom_injective

added theorem CompleteLattice.Independent.linearIndependent

added theorem CompleteLattice.independent_iff_dfinsupp_lsum_injective

added theorem CompleteLattice.independent_iff_dfinsupp_sumAddHom_injective

added theorem CompleteLattice.independent_iff_forall_dfinsupp

added theorem CompleteLattice.independent_iff_linearIndependent_of_ne_zero

added theorem CompleteLattice.independent_of_dfinsupp_lsum_injective

added theorem CompleteLattice.independent_of_dfinsupp_sumAddHom_injective'

added theorem CompleteLattice.independent_of_dfinsupp_sumAddHom_injective

added theorem CompleteLattice.lsum_comp_mapRange_toSpanSingleton

added theorem Dfinsupp.coprodMap_apply

added def Dfinsupp.lapply

added theorem Dfinsupp.lapply_apply

added theorem Dfinsupp.lhom_ext'

added theorem Dfinsupp.lhom_ext

added def Dfinsupp.lmk

added theorem Dfinsupp.lmk_apply

added def Dfinsupp.lsingle

added theorem Dfinsupp.lsingle_apply

added def Dfinsupp.lsum

added theorem Dfinsupp.lsum_single

added def Dfinsupp.mapRange.linearEquiv

added theorem Dfinsupp.mapRange.linearEquiv_refl

added theorem Dfinsupp.mapRange.linearEquiv_symm

added theorem Dfinsupp.mapRange.linearEquiv_trans

added def Dfinsupp.mapRange.linearMap

added theorem Dfinsupp.mapRange.linearMap_comp

added theorem Dfinsupp.mapRange.linearMap_id

added theorem Dfinsupp.mapRange_smul

added theorem Dfinsupp.sum_mapRange_index.linearMap

added theorem Submodule.bsupᵢ_eq_range_dfinsupp_lsum

added theorem Submodule.dfinsupp_sumAddHom_mem

added theorem Submodule.dfinsupp_sum_mem

added theorem Submodule.mem_bsupr_iff_exists_dfinsupp

added theorem Submodule.mem_supᵢ_finset_iff_exists_sum

added theorem Submodule.mem_supᵢ_iff_exists_dfinsupp'

added theorem Submodule.mem_supᵢ_iff_exists_dfinsupp

added theorem Submodule.supᵢ_eq_range_dfinsupp_lsum