Commit 2023-04-06 16:41 da954ad1

View on Github →

feat: port LinearAlgebra.Matrix.DotProduct (#3311)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/DotProduct.lean

added theorem Matrix.dotProduct_eq

added theorem Matrix.dotProduct_eq_iff

added theorem Matrix.dotProduct_eq_zero

added theorem Matrix.dotProduct_eq_zero_iff

added theorem Matrix.dotProduct_stdBasis_eq_mul

added theorem Matrix.dotProduct_stdBasis_one