Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-26 13:06 1f13610e

View on Github →

feat(*): remove the fintype requirement from matrices. (#8810) For historical reasons, matrix has always had fintype attached to it. I remove this artificial limitation, but with a big caveat; multiplication is currently defined in terms of the dot product, which requires finiteness; therefore, any multiplicative structure on matrices currently requires fintypes. This can be removed in future contributions, however.

Estimated changes

modified theorem matrix.add_mul_vec
modified theorem matrix.add_vec_mul
modified theorem matrix.col_mul_vec
modified theorem matrix.col_vec_mul
modified theorem matrix.conj_transpose_mul
modified theorem matrix.diagonal_mul
modified theorem matrix.dot_product_assoc
modified theorem matrix.map_mul
modified theorem matrix.minor_minor
modified theorem matrix.minor_mul
modified theorem matrix.minor_mul_equiv
modified theorem matrix.mul_apply'
modified theorem matrix.mul_apply
modified theorem matrix.mul_diagonal
modified theorem matrix.mul_eq_mul
modified theorem matrix.mul_minor_one
modified theorem matrix.mul_mul_left
modified theorem matrix.mul_smul
modified def matrix.mul_vec
modified theorem matrix.mul_vec_add
modified theorem matrix.mul_vec_diagonal
modified theorem matrix.mul_vec_mul_vec
modified theorem matrix.mul_vec_neg
modified theorem matrix.mul_vec_smul_assoc
modified theorem matrix.mul_vec_transpose
modified theorem matrix.mul_vec_zero
modified theorem matrix.neg_mul_vec
modified theorem matrix.neg_vec_mul
modified theorem matrix.one_minor_mul
modified theorem matrix.one_mul_vec
modified theorem matrix.reindex_trans
modified theorem matrix.row_mul_col_apply
modified theorem matrix.row_mul_vec
modified theorem matrix.row_vec_mul
modified theorem matrix.smul_eq_diagonal_mul
modified theorem matrix.smul_mul
modified theorem matrix.smul_mul_vec_assoc
modified theorem matrix.star_mul
modified theorem matrix.transpose_mul
modified def matrix.vec_mul
modified theorem matrix.vec_mul_add
modified theorem matrix.vec_mul_diagonal
modified theorem matrix.vec_mul_neg
modified theorem matrix.vec_mul_one
modified theorem matrix.vec_mul_transpose
modified theorem matrix.vec_mul_vec_mul
modified theorem matrix.vec_mul_zero
modified theorem matrix.zero_mul_vec
modified theorem matrix.zero_vec_mul
modified def matrix
modified theorem matrix.block_diagonal'_mul
modified theorem matrix.block_diagonal_mul
modified theorem matrix.from_blocks_multiply
modified def matrix.to_block
modified theorem matrix.to_block_apply
modified theorem matrix.mul_kronecker_mul
modified theorem matrix.cons_mul
modified theorem matrix.cons_mul_vec
modified theorem matrix.empty_mul
modified theorem matrix.empty_mul_vec
modified theorem matrix.mul_empty
modified theorem matrix.mul_val_succ
modified theorem matrix.vec_mul_empty
modified theorem pequiv.matrix_mul_apply
modified theorem pequiv.mul_matrix_apply
modified theorem pequiv.single_mul_single
modified theorem pequiv.to_matrix_trans
modified theorem pequiv.to_pequiv_mul_matrix
modified def matrix.to_bilin'_aux
modified theorem basis.to_lin_to_matrix
modified def basis.to_matrix_equiv
modified def alg_equiv_matrix'
modified def alg_equiv_matrix
modified theorem linear_map.to_matrix'_comp
modified theorem linear_map.to_matrix'_mul
modified theorem linear_map.to_matrix_comp
modified def matrix.mul_vec_lin
modified theorem matrix.mul_vec_lin_apply
modified theorem matrix.rank_vec_mul_vec
modified theorem matrix.to_lin'_mul
modified theorem matrix.to_lin'_mul_apply
modified def matrix.to_lin'_of_inv
modified theorem matrix.to_lin_mul
modified theorem matrix.to_lin_mul_apply
modified def matrix.trace