Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-09 22:24 405be36f

View on Github →

feat(data/matrix): Lemmas about vec_mul, mul_vec, dot_product, inv (#14644)

Estimated changes

Modified src/data/matrix/basic.lean

modified theorem matrix.dot_product_assoc

added theorem matrix.mul_vec_vec_mul

added theorem matrix.sub_mul_vec

added theorem matrix.sum_elim_dot_product_sum_elim

added theorem matrix.vec_mul_mul_vec

added theorem matrix.vec_mul_sub

Modified src/data/matrix/block.lean

added theorem matrix.from_blocks_mul_vec

added theorem matrix.vec_mul_from_blocks

Modified src/linear_algebra/matrix/nonsingular_inverse.lean

added theorem matrix.inv_mul_cancel_left_of_invertible

added theorem matrix.inv_mul_cancel_right_of_invertible

added theorem matrix.mul_inv_cancel_left_of_invertible

added theorem matrix.mul_inv_cancel_right_of_invertible

added theorem matrix.mul_nonsing_inv_cancel_left

added theorem matrix.mul_nonsing_inv_cancel_right

added theorem matrix.nonsing_inv_mul_cancel_left

added theorem matrix.nonsing_inv_mul_cancel_right