Commit 2025-03-24 15:47 689ff663

View on Github →

chore(RowCol): rename Matrix.row and Matrix.col (#23150) We rename Matrix.row and Matrix.col to Matrix.replicateRow and Matrix.replicateCol to free up the Matrix.row and Matrix.col identifiers for use as row/column functions of a matrix. renaming poll Zulip review thread

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 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
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