Commit 2024-11-13 19:26 be1dcd60

View on Github →

chore(LinearAlgebra/Finsupp): split Finsupp.lean into many smaller files (#18869) This PR splits up and reorganizes LinearAlgebra/Finsupp.lean into smaller files. The following new files replace the previous Finsupp.lean:

  • Countable.lean: countability of a vector space spanned by a countable family of vectors
  • Finsupp/Defs.lean: for the LinearMap-ifications of basic Finsupp functions such as single
  • Finsupp/LSum.lean: for the LinearMap-ifications of Finsupp.sum and related results
  • Finsupp/LinearCombination.lean: defines Finsupp.linearCombination
  • Finsupp/Pi.lean: results involving the module structure on ⍺ -> β
  • Finsupp/Span.lean: results involving Submodule.span
  • Finsupp/SumProd.lean: results involving the Sum/Prod/Sigma types
  • Finsupp/Supported.lean: defines Finsupp.supported Also rename FinsuppVectorSpace.lean into Finsupp/VectorSpace.lean.

Estimated changes

deleted theorem Finsupp.coe_lsum
deleted theorem Finsupp.domLCongr_apply
deleted theorem Finsupp.domLCongr_refl
deleted theorem Finsupp.domLCongr_single
deleted theorem Finsupp.domLCongr_symm
deleted theorem Finsupp.domLCongr_trans
deleted theorem Finsupp.ker_lsingle
deleted def Finsupp.lapply
deleted theorem Finsupp.lapply_apply
deleted def Finsupp.lcoeFun
deleted def Finsupp.lcongr
deleted theorem Finsupp.lcongr_single
deleted theorem Finsupp.lcongr_symm
deleted theorem Finsupp.lhom_ext'
deleted theorem Finsupp.lhom_ext
deleted theorem Finsupp.lift_apply
deleted theorem Finsupp.lift_symm_apply
deleted theorem Finsupp.llift_apply
deleted theorem Finsupp.llift_symm_apply
deleted def Finsupp.lmapDomain
deleted theorem Finsupp.lmapDomain_apply
deleted theorem Finsupp.lmapDomain_comp
deleted theorem Finsupp.lmapDomain_id
deleted def Finsupp.lsingle
deleted theorem Finsupp.lsingle_apply
deleted def Finsupp.lsum
deleted theorem Finsupp.lsum_apply
deleted theorem Finsupp.lsum_comp_lsingle
deleted theorem Finsupp.lsum_single
deleted theorem Finsupp.lsum_symm_apply
deleted theorem Finsupp.mem_supported'
deleted theorem Finsupp.mem_supported
deleted theorem Finsupp.range_restrictDom
deleted def Finsupp.restrictDom
deleted theorem Finsupp.restrictDom_apply
deleted theorem Finsupp.smul_sum
deleted theorem Finsupp.span_single_image
deleted def Finsupp.supported
deleted theorem Finsupp.supported_empty
deleted theorem Finsupp.supported_iInter
deleted theorem Finsupp.supported_iUnion
deleted theorem Finsupp.supported_inter
deleted theorem Finsupp.supported_mono
deleted theorem Finsupp.supported_union
deleted theorem Finsupp.supported_univ
deleted theorem LinearMap.coe_finsupp_sum
deleted theorem mem_span_finset
deleted theorem mem_span_set'
deleted theorem mem_span_set
deleted theorem span_eq_iUnion_nat
added def Finsupp.lapply
added theorem Finsupp.lapply_apply
added theorem Finsupp.lhom_ext'
added theorem Finsupp.lhom_ext
added theorem Finsupp.lmapDomain_id
added def Finsupp.lsingle
added theorem Finsupp.lsingle_apply
added theorem Finsupp.coe_lsum
added theorem Finsupp.domLCongr_refl
added theorem Finsupp.domLCongr_symm
added def Finsupp.lcongr
added theorem Finsupp.lcongr_single
added theorem Finsupp.lcongr_symm
added theorem Finsupp.lift_apply
added theorem Finsupp.llift_apply
added def Finsupp.lsum
added theorem Finsupp.lsum_apply
added theorem Finsupp.lsum_single
added theorem Finsupp.smul_sum
added theorem mem_span_finset
added theorem mem_span_set'
added theorem mem_span_set
added theorem span_eq_iUnion_nat
added def Finsupp.lcoeFun
added theorem Finsupp.ker_lsingle
added theorem Finsupp.mem_supported'
added theorem Finsupp.mem_supported
added theorem Finsupp.supported_mono
added theorem Finsupp.supported_univ