Commit 2023-04-02 17:01 5483442a

View on Github →

feat: port Data.Matrix.Basic (#2960)

Estimated changes

added def AlgHom.mapMatrix
added theorem AlgHom.mapMatrix_comp
added theorem AlgHom.mapMatrix_id
added def Equiv.mapMatrix
added theorem Equiv.mapMatrix_refl
added theorem Equiv.mapMatrix_symm
added theorem Equiv.mapMatrix_trans
added theorem IsLeftRegular.matrix
added theorem IsSMulRegular.matrix
added theorem LinearMap.mapMatrix_id
added theorem Matrix.add_apply
added theorem Matrix.add_dotProduct
added theorem Matrix.add_mulVec
added theorem Matrix.add_vecMul
added theorem Matrix.bit0_apply
added theorem Matrix.bit1_apply
added theorem Matrix.bit1_apply_eq
added theorem Matrix.bit1_apply_ne
added theorem Matrix.coe_scalar
added def Matrix.col
added theorem Matrix.col_add
added theorem Matrix.col_apply
added theorem Matrix.col_mulVec
added theorem Matrix.col_smul
added theorem Matrix.col_vecMul
added def Matrix.diag
added theorem Matrix.diag_add
added theorem Matrix.diag_apply
added theorem Matrix.diag_diagonal
added theorem Matrix.diag_list_sum
added theorem Matrix.diag_map
added theorem Matrix.diag_neg
added theorem Matrix.diag_one
added theorem Matrix.diag_smul
added theorem Matrix.diag_sub
added theorem Matrix.diag_submatrix
added theorem Matrix.diag_sum
added theorem Matrix.diag_transpose
added theorem Matrix.diag_zero
added def Matrix.diagonal
added theorem Matrix.diagonal_add
added theorem Matrix.diagonal_apply
added theorem Matrix.diagonal_map
added theorem Matrix.diagonal_mul
added theorem Matrix.diagonal_neg
added theorem Matrix.diagonal_one
added theorem Matrix.diagonal_pow
added theorem Matrix.diagonal_smul
added theorem Matrix.diagonal_zero
added theorem Matrix.dotProduct_add
added theorem Matrix.dotProduct_comm
added theorem Matrix.dotProduct_neg
added theorem Matrix.dotProduct_smul
added theorem Matrix.dotProduct_star
added theorem Matrix.dotProduct_sub
added theorem Matrix.dotProduct_zero
added theorem Matrix.ext'
added theorem Matrix.ext
added theorem Matrix.ext_iff
added def Matrix.map
added theorem Matrix.map_algebraMap
added theorem Matrix.map_apply
added theorem Matrix.map_id
added theorem Matrix.map_injective
added theorem Matrix.map_map
added theorem Matrix.map_mul
added theorem Matrix.map_one
added theorem Matrix.map_op_smul'
added theorem Matrix.map_smul'
added theorem Matrix.map_smul
added theorem Matrix.map_updateRow
added def Matrix.mulVec
added theorem Matrix.mulVec_add
added theorem Matrix.mulVec_diagonal
added theorem Matrix.mulVec_mulVec
added theorem Matrix.mulVec_neg
added theorem Matrix.mulVec_single
added theorem Matrix.mulVec_smul
added theorem Matrix.mulVec_vecMul
added theorem Matrix.mulVec_zero
added theorem Matrix.mul_apply'
added theorem Matrix.mul_apply
added theorem Matrix.mul_diagonal
added theorem Matrix.mul_eq_mul
added theorem Matrix.mul_mul_apply
added theorem Matrix.mul_mul_left
added theorem Matrix.mul_mul_right
added theorem Matrix.mul_smul
added theorem Matrix.neg_apply
added theorem Matrix.neg_dotProduct
added theorem Matrix.neg_mulVec
added theorem Matrix.neg_of
added theorem Matrix.neg_vecMul
added def Matrix.of
added theorem Matrix.of_add_of
added theorem Matrix.of_apply
added theorem Matrix.of_sub_of
added theorem Matrix.of_symm_apply
added theorem Matrix.of_zero
added theorem Matrix.one_apply
added theorem Matrix.one_apply_eq
added theorem Matrix.one_apply_ne'
added theorem Matrix.one_apply_ne
added theorem Matrix.one_mulVec
added def Matrix.reindex
added theorem Matrix.reindex_apply
added theorem Matrix.reindex_symm
added theorem Matrix.reindex_trans
added def Matrix.row
added theorem Matrix.row_add
added theorem Matrix.row_apply
added theorem Matrix.row_mulVec
added theorem Matrix.row_smul
added theorem Matrix.row_vecMul
added theorem Matrix.scalar.commute
added def Matrix.scalar
added theorem Matrix.scalar_apply_eq
added theorem Matrix.scalar_apply_ne
added theorem Matrix.scalar_inj
added theorem Matrix.single_vecMul
added theorem Matrix.smul_apply
added theorem Matrix.smul_dotProduct
added theorem Matrix.smul_mul
added theorem Matrix.smul_of
added theorem Matrix.star_apply
added theorem Matrix.star_dotProduct
added theorem Matrix.star_mul
added theorem Matrix.star_mulVec
added theorem Matrix.star_vecMul
added def Matrix.subDown
added def Matrix.subLeft
added def Matrix.subRight
added def Matrix.subUp
added def Matrix.subUpLeft
added theorem Matrix.sub_apply
added theorem Matrix.sub_dotProduct
added theorem Matrix.sub_mulVec
added def Matrix.submatrix
added theorem Matrix.submatrix_add
added theorem Matrix.submatrix_apply
added theorem Matrix.submatrix_id_id
added theorem Matrix.submatrix_map
added theorem Matrix.submatrix_mul
added theorem Matrix.submatrix_neg
added theorem Matrix.submatrix_one
added theorem Matrix.submatrix_smul
added theorem Matrix.submatrix_sub
added theorem Matrix.submatrix_zero
added theorem Matrix.sum_apply
added def Matrix.transpose
added theorem Matrix.transpose_add
added theorem Matrix.transpose_apply
added theorem Matrix.transpose_col
added theorem Matrix.transpose_map
added theorem Matrix.transpose_mul
added theorem Matrix.transpose_neg
added theorem Matrix.transpose_one
added theorem Matrix.transpose_pow
added theorem Matrix.transpose_row
added theorem Matrix.transpose_smul
added theorem Matrix.transpose_sub
added theorem Matrix.transpose_sum
added theorem Matrix.transpose_zero
added theorem Matrix.two_mul_expl
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 def Matrix.vecMul
added def Matrix.vecMulVec
added theorem Matrix.vecMulVec_apply
added theorem Matrix.vecMulVec_eq
added theorem Matrix.vecMul_add
added theorem Matrix.vecMul_diagonal
added theorem Matrix.vecMul_mulVec
added theorem Matrix.vecMul_neg
added theorem Matrix.vecMul_one
added theorem Matrix.vecMul_smul
added theorem Matrix.vecMul_sub
added theorem Matrix.vecMul_vecMul
added theorem Matrix.vecMul_zero
added theorem Matrix.zero_apply
added theorem Matrix.zero_dotProduct
added theorem Matrix.zero_mulVec
added theorem Matrix.zero_vecMul
added def Matrix
added theorem RingHom.mapMatrix_comp
added theorem RingHom.mapMatrix_id
added theorem RingHom.map_dotProduct
added theorem RingHom.map_matrix_mul
added theorem RingHom.map_mulVec
added theorem RingHom.map_vecMul