Commit 2023-11-02 09:33 ee77c382
View on Github →refactor(Data/Matrix/Basic): split row/column decls (#8089)
This splits out row
/col
/updateRow
/updateColumn
to their own file, as Data/Matrix/Basic
is getting rather large.
The copyright comes from https://github.com/leanprover-community/mathlib/pull/1816 and https://github.com/leanprover-community/mathlib/pull/2480
There are no new lemmas in this PR, nor were any existing lemmas deleted.
It's possible that even more lemmas could migrate to this new file (for instance, flipping the import with Matrix.Notation
or LinearAlgebra.Matrix.Trace
), but I've taken the conservative option of leaving those lemmas alone for now.