Commit 2024-11-14 16:12 71e045c8

View on Github →

chore(Data/Matrix): split Basic.lean into Defs.lean and Mul.lean (#18972) This is based on noticing that the definition of Matrix imports Algebra.

  • Defs.lean contains the definition of the Matrix type and its module structure
  • Mul.lean contains vector-and-matrix multiplication operators
  • Basic.lean still contains bundled versions of the operations defined above, and a few lemmas that didn't fit anywhere else.

Estimated changes

deleted theorem IsLeftRegular.matrix
deleted theorem IsSMulRegular.matrix
deleted theorem Matrix.add_apply
deleted theorem Matrix.add_dotProduct
deleted theorem Matrix.add_mulVec
deleted theorem Matrix.add_vecMul
deleted theorem Matrix.coe_ofAddEquiv
deleted def Matrix.diag
deleted theorem Matrix.diag_add
deleted theorem Matrix.diag_apply
deleted theorem Matrix.diag_diagonal
deleted theorem Matrix.diag_map
deleted theorem Matrix.diag_neg
deleted theorem Matrix.diag_one
deleted theorem Matrix.diag_smul
deleted theorem Matrix.diag_sub
deleted theorem Matrix.diag_submatrix
deleted theorem Matrix.diag_transpose
deleted theorem Matrix.diag_zero
deleted def Matrix.diagonal
deleted theorem Matrix.diagonal_add
deleted theorem Matrix.diagonal_apply
deleted theorem Matrix.diagonal_apply_eq
deleted theorem Matrix.diagonal_apply_ne'
deleted theorem Matrix.diagonal_apply_ne
deleted theorem Matrix.diagonal_injective
deleted theorem Matrix.diagonal_intCast'
deleted theorem Matrix.diagonal_intCast
deleted theorem Matrix.diagonal_map
deleted theorem Matrix.diagonal_mul
deleted theorem Matrix.diagonal_natCast'
deleted theorem Matrix.diagonal_natCast
deleted theorem Matrix.diagonal_neg
deleted theorem Matrix.diagonal_ofNat'
deleted theorem Matrix.diagonal_ofNat
deleted theorem Matrix.diagonal_one
deleted theorem Matrix.diagonal_smul
deleted theorem Matrix.diagonal_sub
deleted theorem Matrix.diagonal_transpose
deleted theorem Matrix.diagonal_unique
deleted theorem Matrix.diagonal_zero
deleted def Matrix.dotProduct
deleted theorem Matrix.dotProduct_add
deleted theorem Matrix.dotProduct_assoc
deleted theorem Matrix.dotProduct_comm
deleted theorem Matrix.dotProduct_mulVec
deleted theorem Matrix.dotProduct_neg
deleted theorem Matrix.dotProduct_one
deleted theorem Matrix.dotProduct_pUnit
deleted theorem Matrix.dotProduct_single
deleted theorem Matrix.dotProduct_smul
deleted theorem Matrix.dotProduct_sub
deleted theorem Matrix.dotProduct_zero'
deleted theorem Matrix.dotProduct_zero
deleted theorem Matrix.ext
deleted theorem Matrix.ext_iff
deleted theorem Matrix.intCast_mulVec
deleted def Matrix.map
deleted theorem Matrix.map_apply
deleted theorem Matrix.map_id'
deleted theorem Matrix.map_id
deleted theorem Matrix.map_injective
deleted theorem Matrix.map_map
deleted theorem Matrix.map_mul
deleted theorem Matrix.map_one
deleted theorem Matrix.map_op_smul'
deleted theorem Matrix.map_smul'
deleted theorem Matrix.map_smul
deleted def Matrix.mulVec
deleted theorem Matrix.mulVec_add
deleted theorem Matrix.mulVec_diagonal
deleted theorem Matrix.mulVec_mulVec
deleted theorem Matrix.mulVec_neg
deleted theorem Matrix.mulVec_one
deleted theorem Matrix.mulVec_single
deleted theorem Matrix.mulVec_single_one
deleted theorem Matrix.mulVec_smul
deleted theorem Matrix.mulVec_smul_assoc
deleted theorem Matrix.mulVec_sub
deleted theorem Matrix.mulVec_transpose
deleted theorem Matrix.mulVec_vecMul
deleted theorem Matrix.mulVec_zero
deleted theorem Matrix.mul_apply'
deleted theorem Matrix.mul_apply
deleted theorem Matrix.mul_diagonal
deleted theorem Matrix.mul_mul_apply
deleted theorem Matrix.mul_mul_left
deleted theorem Matrix.mul_mul_right
deleted theorem Matrix.mul_smul
deleted theorem Matrix.mul_submatrix_one
deleted theorem Matrix.natCast_mulVec
deleted theorem Matrix.neg_apply
deleted theorem Matrix.neg_dotProduct
deleted theorem Matrix.neg_dotProduct_neg
deleted theorem Matrix.neg_mulVec
deleted theorem Matrix.neg_mulVec_neg
deleted theorem Matrix.neg_of
deleted theorem Matrix.neg_vecMul
deleted theorem Matrix.neg_vecMul_neg
deleted def Matrix.of
deleted def Matrix.ofAddEquiv
deleted theorem Matrix.ofNat_mulVec
deleted theorem Matrix.of_add_of
deleted theorem Matrix.of_apply
deleted theorem Matrix.of_sub_of
deleted theorem Matrix.of_symm_apply
deleted theorem Matrix.of_zero
deleted theorem Matrix.one_apply
deleted theorem Matrix.one_apply_eq
deleted theorem Matrix.one_apply_ne'
deleted theorem Matrix.one_apply_ne
deleted theorem Matrix.one_dotProduct
deleted theorem Matrix.one_dotProduct_one
deleted theorem Matrix.one_eq_pi_single
deleted theorem Matrix.one_mulVec
deleted theorem Matrix.one_submatrix_mul
deleted def Matrix.reindex
deleted theorem Matrix.reindex_apply
deleted theorem Matrix.reindex_refl_refl
deleted theorem Matrix.reindex_symm
deleted theorem Matrix.reindex_trans
deleted theorem Matrix.single_dotProduct
deleted theorem Matrix.single_one_vecMul
deleted theorem Matrix.single_vecMul
deleted theorem Matrix.smul_apply
deleted theorem Matrix.smul_dotProduct
deleted theorem Matrix.smul_mul
deleted theorem Matrix.smul_mulVec_assoc
deleted theorem Matrix.smul_of
deleted theorem Matrix.sub_apply
deleted theorem Matrix.sub_dotProduct
deleted theorem Matrix.sub_mulVec
deleted theorem Matrix.sub_vecMul
deleted def Matrix.submatrix
deleted theorem Matrix.submatrix_add
deleted theorem Matrix.submatrix_apply
deleted theorem Matrix.submatrix_diagonal
deleted theorem Matrix.submatrix_id_id
deleted theorem Matrix.submatrix_map
deleted theorem Matrix.submatrix_mul
deleted theorem Matrix.submatrix_neg
deleted theorem Matrix.submatrix_one
deleted theorem Matrix.submatrix_smul
deleted theorem Matrix.submatrix_sub
deleted theorem Matrix.submatrix_zero
deleted def Matrix.transpose
deleted theorem Matrix.transpose_add
deleted theorem Matrix.transpose_apply
deleted theorem Matrix.transpose_eq_ofNat
deleted theorem Matrix.transpose_eq_one
deleted theorem Matrix.transpose_eq_zero
deleted theorem Matrix.transpose_inj
deleted theorem Matrix.transpose_intCast
deleted theorem Matrix.transpose_map
deleted theorem Matrix.transpose_mul
deleted theorem Matrix.transpose_natCast
deleted theorem Matrix.transpose_neg
deleted theorem Matrix.transpose_ofNat
deleted theorem Matrix.transpose_one
deleted theorem Matrix.transpose_reindex
deleted theorem Matrix.transpose_smul
deleted theorem Matrix.transpose_sub
deleted theorem Matrix.transpose_zero
deleted theorem Matrix.two_mul_expl
deleted def Matrix.vecMul
deleted def Matrix.vecMulVec
deleted theorem Matrix.vecMulVec_apply
deleted theorem Matrix.vecMul_add
deleted theorem Matrix.vecMul_diagonal
deleted theorem Matrix.vecMul_intCast
deleted theorem Matrix.vecMul_mulVec
deleted theorem Matrix.vecMul_natCast
deleted theorem Matrix.vecMul_neg
deleted theorem Matrix.vecMul_ofNat
deleted theorem Matrix.vecMul_one
deleted theorem Matrix.vecMul_smul
deleted theorem Matrix.vecMul_sub
deleted theorem Matrix.vecMul_transpose
deleted theorem Matrix.vecMul_vecMul
deleted theorem Matrix.vecMul_zero
deleted theorem Matrix.vec_one_mul
deleted theorem Matrix.zero_apply
deleted theorem Matrix.zero_dotProduct'
deleted theorem Matrix.zero_dotProduct
deleted theorem Matrix.zero_mulVec
deleted theorem Matrix.zero_vecMul
deleted def Matrix
deleted theorem RingHom.map_dotProduct
deleted theorem RingHom.map_matrix_mul
deleted theorem RingHom.map_mulVec
deleted theorem RingHom.map_vecMul
added theorem IsLeftRegular.matrix
added theorem IsSMulRegular.matrix
added theorem Matrix.add_apply
added theorem Matrix.coe_ofAddEquiv
added theorem Matrix.ext
added theorem Matrix.ext_iff
added def Matrix.map
added theorem Matrix.map_apply
added theorem Matrix.map_id'
added theorem Matrix.map_id
added theorem Matrix.map_injective
added theorem Matrix.map_map
added theorem Matrix.map_op_smul'
added theorem Matrix.map_smul'
added theorem Matrix.map_smul
added theorem Matrix.neg_apply
added theorem Matrix.neg_of
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 def Matrix.reindex
added theorem Matrix.reindex_apply
added theorem Matrix.reindex_symm
added theorem Matrix.reindex_trans
added theorem Matrix.smul_apply
added theorem Matrix.smul_of
added theorem Matrix.sub_apply
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_neg
added theorem Matrix.submatrix_smul
added theorem Matrix.submatrix_sub
added theorem Matrix.submatrix_zero
added def Matrix.transpose
added theorem Matrix.transpose_add
added theorem Matrix.transpose_apply
added theorem Matrix.transpose_inj
added theorem Matrix.transpose_map
added theorem Matrix.transpose_neg
added theorem Matrix.transpose_smul
added theorem Matrix.transpose_sub
added theorem Matrix.transpose_zero
added theorem Matrix.zero_apply
added def Matrix
added def Matrix.diag
added theorem Matrix.diag_add
added theorem Matrix.diag_apply
added theorem Matrix.diag_diagonal
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_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_neg
added theorem Matrix.diagonal_ofNat'
added theorem Matrix.diagonal_ofNat
added theorem Matrix.diagonal_one
added theorem Matrix.diagonal_smul
added theorem Matrix.diagonal_sub
added theorem Matrix.diagonal_unique
added theorem Matrix.diagonal_zero
added theorem Matrix.map_one
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.submatrix_one
added theorem Matrix.transpose_ofNat
added theorem Matrix.transpose_one
added theorem Matrix.add_dotProduct
added theorem Matrix.add_mulVec
added theorem Matrix.add_vecMul
added theorem Matrix.diagonal_mul
added theorem Matrix.dotProduct_add
added theorem Matrix.dotProduct_comm
added theorem Matrix.dotProduct_neg
added theorem Matrix.dotProduct_one
added theorem Matrix.dotProduct_smul
added theorem Matrix.dotProduct_sub
added theorem Matrix.dotProduct_zero
added theorem Matrix.intCast_mulVec
added theorem Matrix.map_mul
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_one
added theorem Matrix.mulVec_single
added theorem Matrix.mulVec_smul
added theorem Matrix.mulVec_sub
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_mul_apply
added theorem Matrix.mul_mul_left
added theorem Matrix.mul_mul_right
added theorem Matrix.mul_smul
added theorem Matrix.natCast_mulVec
added theorem Matrix.neg_dotProduct
added theorem Matrix.neg_mulVec
added theorem Matrix.neg_mulVec_neg
added theorem Matrix.neg_vecMul
added theorem Matrix.neg_vecMul_neg
added theorem Matrix.ofNat_mulVec
added theorem Matrix.one_dotProduct
added theorem Matrix.one_mulVec
added theorem Matrix.single_vecMul
added theorem Matrix.smul_dotProduct
added theorem Matrix.smul_mul
added theorem Matrix.sub_dotProduct
added theorem Matrix.sub_mulVec
added theorem Matrix.sub_vecMul
added theorem Matrix.submatrix_mul
added theorem Matrix.transpose_mul
added theorem Matrix.two_mul_expl
added def Matrix.vecMul
added def Matrix.vecMulVec
added theorem Matrix.vecMulVec_apply
added theorem Matrix.vecMul_add
added theorem Matrix.vecMul_diagonal
added theorem Matrix.vecMul_intCast
added theorem Matrix.vecMul_mulVec
added theorem Matrix.vecMul_natCast
added theorem Matrix.vecMul_neg
added theorem Matrix.vecMul_ofNat
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.vec_one_mul
added theorem Matrix.zero_dotProduct
added theorem Matrix.zero_mulVec
added theorem Matrix.zero_vecMul
added theorem RingHom.map_dotProduct
added theorem RingHom.map_matrix_mul
added theorem RingHom.map_mulVec
added theorem RingHom.map_vecMul