Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-04-21 14:26 eba5bb31

View on Github →

feat(data/matrix/basic): miscellaneous defs and lemmas (#8289) miscellaneous defs and lemmas

Estimated changes

Modified src/data/matrix/basic.lean

added theorem matrix.dot_product_one

modified theorem matrix.mul_submatrix_one

added theorem matrix.mul_vec_one

added theorem matrix.one_dot_product

added theorem matrix.one_dot_product_one

modified theorem matrix.one_submatrix_mul

added theorem matrix.vec_one_mul

Modified src/data/matrix/block.lean

added theorem matrix.dot_product_block