Commit 2024-05-16 19:48 732a2b8a

View on Github →

feat (Data/Matrix/Basic): Matrix versions of neg_mul_neg (#12901)

Estimated changes

Modified Mathlib/Data/Matrix/Basic.lean

added theorem Matrix.neg_dotProduct_neg

added theorem Matrix.neg_mulVec_neg

added theorem Matrix.neg_vecMul_neg