refactor(data/matrix,linear_algebra): Use matrix.mul as default mul…

…tiplication 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

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

src/data/matrix/basic.lean

@@ -174,13 +174,13 @@ instance [decidable_eq n] : semiring (matrix n n α) :=
   ..matrix.add_comm_monoid,
   ..matrix.monoid }
 
-@[simp] theorem diagonal_mul_diagonal' [decidable_eq n] (d₁ d₂ : n → α) :
+@[simp] theorem diagonal_mul_diagonal [decidable_eq n] (d₁ d₂ : n → α) :
   (diagonal d₁) ⬝ (diagonal d₂) = diagonal (λ i, d₁ i * d₂ i) :=
 by ext i j; by_cases i = j; simp [h]
 
-theorem diagonal_mul_diagonal [decidable_eq n] (d₁ d₂ : n → α) :
+theorem diagonal_mul_diagonal' [decidable_eq n] (d₁ d₂ : n → α) :
   diagonal d₁ * diagonal d₂ = diagonal (λ i, d₁ i * d₂ i) :=
-diagonal_mul_diagonal' _ _
+diagonal_mul_diagonal _ _
 
 lemma is_add_monoid_hom_mul_left (M : matrix l m α) :
   is_add_monoid_hom (λ x : matrix m n α, M ⬝ x) :=

src/data/matrix/pequiv.lean

@@ -76,9 +76,9 @@ begin
     simp [h, eq_comm] {contextual := tt} }
 end
 
-lemma to_pequiv_mul_matrix [semiring α] (f : n ≃ n) (M : matrix n n α) :
-  (f.to_pequiv.to_matrix * M) = λ i, M (f i) :=
-by { ext i j, rw [mul_eq_mul, mul_matrix_apply, equiv.to_pequiv_apply] }
+lemma to_pequiv_mul_matrix [semiring α] (f : m ≃ m) (M : matrix m n α) :
+  (f.to_pequiv.to_matrix ⬝ M) = λ i, M (f i) :=
+by { ext i j, rw [mul_matrix_apply, equiv.to_pequiv_apply] }
 
 lemma to_matrix_trans [semiring α] (f : l ≃. m) (g : m ≃. n) :
   ((f.trans g).to_matrix : matrix l n α) = f.to_matrix ⬝ g.to_matrix :=

src/linear_algebra/determinant.lean

@@ -11,6 +11,7 @@ universes u v
 open equiv equiv.perm finset function
 
 namespace matrix
+open_locale matrix
 
 variables {n : Type u} [fintype n] [decidable_eq n] {R : Type v} [comm_ring R]
 
@@ -68,11 +69,11 @@ begin
     (λ _ _, equiv.ext _ _ $ by simp)
 end
 
-@[simp] lemma det_mul (M N : matrix n n R) : det (M * N) = det M * det N :=
-calc det (M * N) = univ.sum (λ σ : perm n, (univ.pi (λ a, univ)).sum
+@[simp] lemma det_mul (M N : matrix n n R) : det (M ⬝ N) = det M * det N :=
+calc det (M ⬝ N) = univ.sum (λ σ : perm n, (univ.pi (λ a, univ)).sum
     (λ (p : Π (a : n), a ∈ univ → n), ε σ *
     univ.attach.prod (λ i, M (σ i.1) (p i.1 (mem_univ _)) * N (p i.1 (mem_univ _)) i.1))) :
-  by simp only [det, mul_val', prod_sum, mul_sum]
+  by simp only [det, mul_val, prod_sum, mul_sum]
 ... = univ.sum (λ σ : perm n, univ.sum
     (λ p : n → n, ε σ * univ.prod (λ i, M (σ i) (p i) * N (p i) i))) :
   sum_congr rfl (λ σ _, sum_bij
@@ -113,7 +114,7 @@ instance : is_monoid_hom (det : matrix n n R → R) :=
   map_mul := det_mul }
 
 /-- Transposing a matrix preserves the determinant. -/
-@[simp] lemma det_transpose (M : matrix n n R) : M.transpose.det = M.det :=
+@[simp] lemma det_transpose (M : matrix n n R) : Mᵀ.det = M.det :=
 begin
   apply sum_bij (λ σ _, σ⁻¹),
   { intros σ _, apply mem_univ },