Matrix multiplication and summations

Stream: Is there code for X?

[Christopher Lynch]

I am new to Lean, so I hope this question is not too stupid.

We are trying to prove the correctness of Gaussian Elimination, as it is one or the undergraduate math topics missing in Mathlib. So we need to relate define row operations in Lean and relate them to matrix multiplications. But I don't now how to handle the details of matrix multiplication. I have condensed my code to the following:

import Mathlib

-- Copies Row j to Row i, used in SwapRow
def dupRow [DecidableEq m] (M : Matrix m n α) (i : m) (j : m) : Matrix m n α :=
  Matrix.updateRow M i (M j)

-- Operation with swaps Row i and j
def swapRow [DecidableEq m] (M : Matrix m n α) (i : m) (j : m) : Matrix m n α :=
  Matrix.updateRow (dupRow M i j) j (M i)

-- If you swap Row i and j then Row i will be the previous Row j
lemma swapRowi [DecidableEq m](M : Matrix m n α) (i : m) (j : m)
  : swapRow M i j i = M j := by sorry

variable [MulOneClass α] [AddCommMonoid α]

theorem swapMatEqSwap [DecidableEq n]
  [Fintype n]
  (M : Matrix n n ℝ) (i : n) (j : n)
  : swapRow (1 : Matrix n n ℝ) i j * M = swapRow M i j := by
  ext p q
  by_cases peqi : p = i
  rw [peqi, swapRowi]
  rw [Matrix.mul_apply, swapRowi]

In the theorem, I need to prove :

(Finset.univ.sum fun j_1 => 1 j j_1 * M j_1 q) = M j q

But I don't know how to operate on this summation. I tried

rw [Matrix.one_apply]

hoping this would reduce 1 j j_1 to an if then else statement, which I was hoping to simplify. But that rewrite did not work. I guess that was because I was trying to rewrite inside the summation. The only other idea I had was finset induction, but I can't find a reference on how to do that. I am guessing that is not necessary though.

As a second question, I have defined the matrix as a matrix of real numbers. I would like to generalize it though. Before the theorem I have defined some type classes for alpha, and then I would like to have a matrix of type alpha. But I think other type classes may be necessary.

Thanks for any help.

[Kevin Buzzard]

Try simp_rw for rewriting under binders.

[Christopher Lynch]

That worked perfectly. Thank you.

[Kevin Buzzard]

I don't really know why they don't just make rw work in these situations (but no doubt there are reasons).

[Christopher Lynch]

I googled simp_rw, and I found a comment about how it can go into an infinite loop but rw cannot. That might be a reason.

By the way, your notes "Formalizing Mathematics" are a great resource for when I know what I want to do but I don't know how to write it in Lean. Now I see that you actually talked about simp_rw in those notes. If I had seen that first, I wouldn't have had to ask.

[Kevin Buzzard]

There's so many tricks to learn!