Commit 2024-01-15 14:51 18cc8db1

View on Github →

Matrix.dotProduct inequalities (#9652)

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/DotProduct.lean

added theorem Matrix.dotProduct_le_dotProduct_of_nonneg_left

added theorem Matrix.dotProduct_le_dotProduct_of_nonneg_right

added theorem Matrix.dotProduct_nonneg_of_nonneg