Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-04-02 17:01
5483442a
View on Github →
feat: port Data.Matrix.Basic (
#2960
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Data/Matrix/Basic.lean
added
def
AddEquiv.mapMatrix
added
theorem
AddEquiv.mapMatrix_refl
added
theorem
AddEquiv.mapMatrix_symm
added
theorem
AddEquiv.mapMatrix_trans
added
def
AddMonoidHom.mapMatrix
added
theorem
AddMonoidHom.mapMatrix_comp
added
theorem
AddMonoidHom.mapMatrix_id
added
def
AlgEquiv.mapMatrix
added
theorem
AlgEquiv.mapMatrix_refl
added
theorem
AlgEquiv.mapMatrix_symm
added
theorem
AlgEquiv.mapMatrix_trans
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
def
LinearEquiv.mapMatrix
added
theorem
LinearEquiv.mapMatrix_refl
added
theorem
LinearEquiv.mapMatrix_symm
added
theorem
LinearEquiv.mapMatrix_trans
added
def
LinearMap.mapMatrix
added
theorem
LinearMap.mapMatrix_comp
added
theorem
LinearMap.mapMatrix_id
added
def
Matrix.addMonoidHomMulLeft
added
def
Matrix.addMonoidHomMulRight
added
theorem
Matrix.add_apply
added
theorem
Matrix.add_dotProduct
added
theorem
Matrix.add_mulVec
added
theorem
Matrix.add_vecMul
added
theorem
Matrix.algebraMap_eq_diagonal
added
theorem
Matrix.algebraMap_eq_diagonalRingHom
added
theorem
Matrix.algebraMap_eq_smul
added
theorem
Matrix.algebraMap_matrix_apply
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.conjTranspose
added
def
Matrix.conjTransposeAddEquiv
added
theorem
Matrix.conjTransposeAddEquiv_symm
added
def
Matrix.conjTransposeLinearEquiv
added
theorem
Matrix.conjTransposeLinearEquiv_symm
added
def
Matrix.conjTransposeRingEquiv
added
theorem
Matrix.conjTranspose_add
added
theorem
Matrix.conjTranspose_apply
added
theorem
Matrix.conjTranspose_col
added
theorem
Matrix.conjTranspose_conjTranspose
added
theorem
Matrix.conjTranspose_intCast_smul
added
theorem
Matrix.conjTranspose_inv_intCast_smul
added
theorem
Matrix.conjTranspose_inv_natCast_smul
added
theorem
Matrix.conjTranspose_list_prod
added
theorem
Matrix.conjTranspose_list_sum
added
theorem
Matrix.conjTranspose_map
added
theorem
Matrix.conjTranspose_mul
added
theorem
Matrix.conjTranspose_multiset_sum
added
theorem
Matrix.conjTranspose_natCast_smul
added
theorem
Matrix.conjTranspose_neg
added
theorem
Matrix.conjTranspose_nsmul
added
theorem
Matrix.conjTranspose_one
added
theorem
Matrix.conjTranspose_pow
added
theorem
Matrix.conjTranspose_ratCast_smul
added
theorem
Matrix.conjTranspose_rat_smul
added
theorem
Matrix.conjTranspose_reindex
added
theorem
Matrix.conjTranspose_row
added
theorem
Matrix.conjTranspose_smul
added
theorem
Matrix.conjTranspose_smul_non_comm
added
theorem
Matrix.conjTranspose_smul_self
added
theorem
Matrix.conjTranspose_sub
added
theorem
Matrix.conjTranspose_submatrix
added
theorem
Matrix.conjTranspose_sum
added
theorem
Matrix.conjTranspose_zero
added
theorem
Matrix.conjTranspose_zsmul
added
def
Matrix.diag
added
def
Matrix.diagAddMonoidHom
added
def
Matrix.diagLinearMap
added
theorem
Matrix.diag_add
added
theorem
Matrix.diag_apply
added
theorem
Matrix.diag_col_mul_row
added
theorem
Matrix.diag_conjTranspose
added
theorem
Matrix.diag_diagonal
added
theorem
Matrix.diag_list_sum
added
theorem
Matrix.diag_map
added
theorem
Matrix.diag_multiset_sum
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
def
Matrix.diagonalAddMonoidHom
added
def
Matrix.diagonalAlgHom
added
def
Matrix.diagonalLinearMap
added
def
Matrix.diagonalRingHom
added
theorem
Matrix.diagonal_add
added
theorem
Matrix.diagonal_apply
added
theorem
Matrix.diagonal_apply_eq
added
theorem
Matrix.diagonal_apply_ne'
added
theorem
Matrix.diagonal_apply_ne
added
theorem
Matrix.diagonal_conjTranspose
added
theorem
Matrix.diagonal_dotProduct
added
theorem
Matrix.diagonal_eq_diagonal_iff
added
theorem
Matrix.diagonal_injective
added
theorem
Matrix.diagonal_map
added
theorem
Matrix.diagonal_mul
added
theorem
Matrix.diagonal_mulVec_single
added
theorem
Matrix.diagonal_mul_diagonal'
added
theorem
Matrix.diagonal_mul_diagonal
added
theorem
Matrix.diagonal_neg
added
theorem
Matrix.diagonal_one
added
theorem
Matrix.diagonal_pow
added
theorem
Matrix.diagonal_smul
added
theorem
Matrix.diagonal_transpose
added
theorem
Matrix.diagonal_updateColumn_single
added
theorem
Matrix.diagonal_updateRow_single
added
theorem
Matrix.diagonal_zero
added
def
Matrix.dotProduct
added
theorem
Matrix.dotProduct_add
added
theorem
Matrix.dotProduct_assoc
added
theorem
Matrix.dotProduct_comm
added
theorem
Matrix.dotProduct_diagonal'
added
theorem
Matrix.dotProduct_diagonal
added
theorem
Matrix.dotProduct_mulVec
added
theorem
Matrix.dotProduct_neg
added
theorem
Matrix.dotProduct_pUnit
added
theorem
Matrix.dotProduct_single
added
theorem
Matrix.dotProduct_smul
added
theorem
Matrix.dotProduct_star
added
theorem
Matrix.dotProduct_sub
added
theorem
Matrix.dotProduct_zero'
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_updateColumn
added
theorem
Matrix.map_updateRow
added
def
Matrix.mulVec.addMonoidHomLeft
added
def
Matrix.mulVec
added
theorem
Matrix.mulVec_add
added
theorem
Matrix.mulVec_conjTranspose
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_smul_assoc
added
theorem
Matrix.mulVec_transpose
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.mul_submatrix_one
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_eq_pi_single
added
theorem
Matrix.one_mulVec
added
theorem
Matrix.one_submatrix_mul
added
def
Matrix.reindex
added
theorem
Matrix.reindex_apply
added
theorem
Matrix.reindex_refl_refl
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_mul_col_apply
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_dotProduct
added
theorem
Matrix.single_vecMul
added
theorem
Matrix.single_vecMul_diagonal
added
theorem
Matrix.smul_apply
added
theorem
Matrix.smul_dotProduct
added
theorem
Matrix.smul_eq_diagonal_mul
added
theorem
Matrix.smul_eq_mul_diagonal
added
theorem
Matrix.smul_mul
added
theorem
Matrix.smul_mulVec_assoc
added
theorem
Matrix.smul_of
added
theorem
Matrix.star_apply
added
theorem
Matrix.star_dotProduct
added
theorem
Matrix.star_dotProduct_star
added
theorem
Matrix.star_eq_conjTranspose
added
theorem
Matrix.star_mul
added
theorem
Matrix.star_mulVec
added
theorem
Matrix.star_vecMul
added
def
Matrix.subDown
added
def
Matrix.subDownLeft
added
def
Matrix.subDownRight
added
def
Matrix.subLeft
added
def
Matrix.subRight
added
def
Matrix.subUp
added
def
Matrix.subUpLeft
added
def
Matrix.subUpRight
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_diagonal
added
theorem
Matrix.submatrix_diagonal_embedding
added
theorem
Matrix.submatrix_diagonal_equiv
added
theorem
Matrix.submatrix_id_id
added
theorem
Matrix.submatrix_map
added
theorem
Matrix.submatrix_mul
added
theorem
Matrix.submatrix_mul_equiv
added
theorem
Matrix.submatrix_mul_transpose_submatrix
added
theorem
Matrix.submatrix_neg
added
theorem
Matrix.submatrix_one
added
theorem
Matrix.submatrix_one_embedding
added
theorem
Matrix.submatrix_one_equiv
added
theorem
Matrix.submatrix_smul
added
theorem
Matrix.submatrix_sub
added
theorem
Matrix.submatrix_submatrix
added
theorem
Matrix.submatrix_zero
added
theorem
Matrix.sum_apply
added
theorem
Matrix.sum_elim_dotProduct_sum_elim
added
def
Matrix.transpose
added
def
Matrix.transposeAddEquiv
added
theorem
Matrix.transposeAddEquiv_symm
added
def
Matrix.transposeAlgEquiv
added
def
Matrix.transposeLinearEquiv
added
theorem
Matrix.transposeLinearEquiv_symm
added
def
Matrix.transposeRingEquiv
added
theorem
Matrix.transpose_add
added
theorem
Matrix.transpose_apply
added
theorem
Matrix.transpose_col
added
theorem
Matrix.transpose_list_prod
added
theorem
Matrix.transpose_list_sum
added
theorem
Matrix.transpose_map
added
theorem
Matrix.transpose_mul
added
theorem
Matrix.transpose_multiset_sum
added
theorem
Matrix.transpose_neg
added
theorem
Matrix.transpose_one
added
theorem
Matrix.transpose_pow
added
theorem
Matrix.transpose_reindex
added
theorem
Matrix.transpose_row
added
theorem
Matrix.transpose_smul
added
theorem
Matrix.transpose_sub
added
theorem
Matrix.transpose_submatrix
added
theorem
Matrix.transpose_sum
added
theorem
Matrix.transpose_transpose
added
theorem
Matrix.transpose_zero
added
theorem
Matrix.two_mul_expl
added
def
Matrix.updateColumn
added
theorem
Matrix.updateColumn_apply
added
theorem
Matrix.updateColumn_conjTranspose
added
theorem
Matrix.updateColumn_eq_self
added
theorem
Matrix.updateColumn_ne
added
theorem
Matrix.updateColumn_self
added
theorem
Matrix.updateColumn_subsingleton
added
theorem
Matrix.updateColumn_transpose
added
def
Matrix.updateRow
added
theorem
Matrix.updateRow_apply
added
theorem
Matrix.updateRow_conjTranspose
added
theorem
Matrix.updateRow_eq_self
added
theorem
Matrix.updateRow_ne
added
theorem
Matrix.updateRow_self
added
theorem
Matrix.updateRow_subsingleton
added
theorem
Matrix.updateRow_transpose
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_conjTranspose
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_transpose
added
theorem
Matrix.vecMul_vecMul
added
theorem
Matrix.vecMul_zero
added
theorem
Matrix.zero_apply
added
theorem
Matrix.zero_dotProduct'
added
theorem
Matrix.zero_dotProduct
added
theorem
Matrix.zero_mulVec
added
theorem
Matrix.zero_vecMul
added
def
Matrix
added
def
RingEquiv.mapMatrix
added
theorem
RingEquiv.mapMatrix_refl
added
theorem
RingEquiv.mapMatrix_symm
added
theorem
RingEquiv.mapMatrix_trans
added
def
RingHom.mapMatrix
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
Modified
Mathlib/GroupTheory/GroupAction/Pi.lean