mathlib

61c095f2 - chore(algebra/module,linear_algebra): split off a `linear_map` file (#4476)

chore(algebra/module,linear_algebra): split off a `linear_map` file (#4476) In order to make `algebra/module/basic.lean` and `linear_algebra/basic.lean` a bit more manageable, move the basic facts about `linear_map`s and `linear_equiv`s into a separate file. `linear_algebra/basic.lean` still needs to be split a bit more.