Commit 2020-11-02 18:45 13a104d9

View on Github →

chore({data,linear_algebra}/dfinsupp): Move linear_algebra stuff to its own file (#4873) This makes the layout of files about dfinsupp resemble those of finsupp a little better. This also:

Renames type arguments to match the names of those in finsupp
Adjusts argument explicitness to match those in finsupp
Adds dfinsupp.lapply to match finsupp.lapply

Estimated changes

Modified src/data/dfinsupp.lean

deleted theorem dfinsupp.lhom_ext'

deleted theorem dfinsupp.lhom_ext

deleted def dfinsupp.lmk

deleted theorem dfinsupp.lmk_apply

deleted def dfinsupp.lsingle

deleted theorem dfinsupp.lsingle_apply

deleted def dfinsupp.lsum

Created src/linear_algebra/dfinsupp.lean

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

Modified src/linear_algebra/direct_sum_module.lean

Modified src/linear_algebra/finsupp.lean