Commit 2023-04-24 00:27 67d9267c

View on Github →

feat: Miscellaneous defs and lemmas (#3589) Match https://github.com/leanprover-community/mathlib/pull/8289

Estimated changes

added theorem Matrix.dotProduct_one
added theorem Matrix.mulVec_one
modified theorem Matrix.mul_submatrix_one
added theorem Matrix.one_dotProduct
modified theorem Matrix.one_submatrix_mul
added theorem Matrix.vec_one_mul