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.