Commit 2024-06-20 12:08 a6fc8cb4

View on Github →

feat(Data/Matrix/RowCol): generalise the Unique indexing type in Matrix.row and Matrix.col (#11536) Changing Matrix.row and Matrix.col to use arbitrary Unique type for indexing the single column/row.

Estimated changes

modified theorem Matrix.frobenius_nnnorm_col
modified theorem Matrix.frobenius_nnnorm_row
modified theorem Matrix.frobenius_norm_col
modified theorem Matrix.frobenius_norm_row
modified theorem Matrix.linfty_opNNNorm_col
modified theorem Matrix.linfty_opNNNorm_row
modified theorem Matrix.linfty_opNorm_col
modified theorem Matrix.linfty_opNorm_row
modified theorem Matrix.nnnorm_col
modified theorem Matrix.nnnorm_row
modified theorem Matrix.norm_col
modified theorem Matrix.norm_row
modified theorem Matrix.col_empty
modified theorem Matrix.row_cons
modified theorem Matrix.row_empty
modified def Matrix.col
modified theorem Matrix.col_add
modified theorem Matrix.col_apply
modified theorem Matrix.col_eq_zero
modified theorem Matrix.col_inj
modified theorem Matrix.col_injective
modified theorem Matrix.col_smul
modified theorem Matrix.col_zero
modified theorem Matrix.conjTranspose_col
modified theorem Matrix.conjTranspose_row
modified theorem Matrix.diag_col_mul_row
modified def Matrix.row
modified theorem Matrix.row_add
modified theorem Matrix.row_apply
modified theorem Matrix.row_eq_zero
modified theorem Matrix.row_inj
modified theorem Matrix.row_injective
modified theorem Matrix.row_smul
modified theorem Matrix.row_zero
modified theorem Matrix.transpose_col
modified theorem Matrix.transpose_row
modified theorem Matrix.vecMulVec_eq
modified theorem Matrix.det_add_col_mul_row
modified theorem Matrix.trace_col_mul_row
modified theorem Continuous.matrix_col
modified theorem Continuous.matrix_row