mathlib

13a104d9 - chore({data,linear_algebra}/dfinsupp): Move linear_algebra stuff to its own file (#4873)

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`