# Commit 2020-10-26 18:39 61c095f2

View on Github →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.