Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-09 09:33 777f2141

View on Github →

refactor(data/matrix,linear_algebra): Use matrix.mul as default multiplication in matrix lemmas (#1959)

  • Change has_mul.mul to matrix.mul in a few simp lemmas
  • Standardise more lemmas for matrix multiplication
  • Generalize to_pequiv_mul_matrix to rectangular matrices

Estimated changes

modified theorem pequiv.to_pequiv_mul_matrix
modified theorem matrix.det_mul
modified theorem matrix.det_transpose