Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-21 14:25 9ce032c3

View on Github →

feat(data/matrix/basic): generalize to non_assoc_semiring (#7974) Matrices with whose coefficients form a non-unital and/or non-associative ring themselves form a non-unital and non-associative ring. This isn't a full generalization of the file, the main aim was to generalize the typeclass instances available.

Estimated changes

modified theorem finset.sum_boole
modified theorem ring_hom.map_list_sum
modified theorem ring_hom.map_multiset_sum
modified theorem ring_hom.map_sum
modified theorem matrix.add_dot_product
modified theorem matrix.col_add
modified theorem matrix.col_smul
modified theorem matrix.diagonal_dot_product
modified theorem matrix.dot_product_add
modified theorem matrix.dot_product_assoc
modified theorem matrix.dot_product_diagonal
modified theorem matrix.dot_product_smul
modified theorem matrix.dot_product_zero'
modified theorem matrix.dot_product_zero
modified theorem matrix.map_mul
modified theorem matrix.row_add
modified theorem matrix.row_mul_col_apply
modified theorem matrix.row_smul
modified theorem matrix.smul_dot_product
modified theorem matrix.smul_mul_vec_assoc
added theorem matrix.sum_apply
modified def matrix.vec_mul_vec
modified theorem matrix.zero_dot_product'
modified theorem matrix.zero_dot_product