Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-05 04:01 858d111c

View on Github →

feat(data/matrix): more basic matrix lemmas (#873)

  • feat(data/matrix): more basic matrix lemmas
  • feat(data/matrix): transpose_add

Estimated changes

modified theorem matrix.add_mul
modified theorem matrix.mul_add
added theorem matrix.mul_neg
added theorem matrix.mul_smul
modified theorem matrix.mul_zero
added theorem matrix.neg_mul
added theorem matrix.smul_mul
added theorem matrix.transpose_add
added theorem matrix.transpose_mul
added theorem matrix.transpose_neg
added theorem matrix.transpose_zero
modified theorem matrix.zero_mul