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.

Estimated changes

deleted def Matrix.col
deleted theorem Matrix.col_add
deleted theorem Matrix.col_apply
deleted theorem Matrix.col_eq_zero
deleted theorem Matrix.col_inj
deleted theorem Matrix.col_injective
deleted theorem Matrix.col_mulVec
deleted theorem Matrix.col_smul
deleted theorem Matrix.col_vecMul
deleted theorem Matrix.col_zero
deleted theorem Matrix.conjTranspose_col
deleted theorem Matrix.conjTranspose_row
deleted theorem Matrix.diag_col_mul_row
deleted theorem Matrix.map_updateColumn
deleted theorem Matrix.map_updateRow
deleted theorem Matrix.reindex_updateRow
deleted def Matrix.row
deleted theorem Matrix.row_add
deleted theorem Matrix.row_apply
deleted theorem Matrix.row_eq_zero
deleted theorem Matrix.row_inj
deleted theorem Matrix.row_injective
deleted theorem Matrix.row_mulVec
deleted theorem Matrix.row_mul_col_apply
deleted theorem Matrix.row_smul
deleted theorem Matrix.row_vecMul
deleted theorem Matrix.row_zero
deleted theorem Matrix.transpose_col
deleted theorem Matrix.transpose_row
deleted def Matrix.updateColumn
deleted theorem Matrix.updateColumn_apply
deleted theorem Matrix.updateColumn_ne
deleted theorem Matrix.updateColumn_self
deleted def Matrix.updateRow
deleted theorem Matrix.updateRow_apply
deleted theorem Matrix.updateRow_eq_self
deleted theorem Matrix.updateRow_ne
deleted theorem Matrix.updateRow_reindex
deleted theorem Matrix.updateRow_self
deleted theorem Matrix.vecMulVec_eq
added def Matrix.col
added theorem Matrix.col_add
added theorem Matrix.col_apply
added theorem Matrix.col_eq_zero
added theorem Matrix.col_inj
added theorem Matrix.col_injective
added theorem Matrix.col_mulVec
added theorem Matrix.col_smul
added theorem Matrix.col_vecMul
added theorem Matrix.col_zero
added theorem Matrix.map_updateRow
added def Matrix.row
added theorem Matrix.row_add
added theorem Matrix.row_apply
added theorem Matrix.row_eq_zero
added theorem Matrix.row_inj
added theorem Matrix.row_injective
added theorem Matrix.row_mulVec
added theorem Matrix.row_smul
added theorem Matrix.row_vecMul
added theorem Matrix.row_zero
added theorem Matrix.transpose_col
added theorem Matrix.transpose_row
added theorem Matrix.updateColumn_ne
added def Matrix.updateRow
added theorem Matrix.updateRow_apply
added theorem Matrix.updateRow_ne
added theorem Matrix.updateRow_self
added theorem Matrix.vecMulVec_eq