Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-31 13:28 53680f96

View on Github →

feat(data/matrix): mul_sum and sum_mul (#1253)

  • feat(data/matrix): mul_sum and sum_mul
  • Update matrix.lean
  • add comment explaing funny proof

Estimated changes