## Stream: new members

### Topic: update_row and update_column

#### Yakov Pechersky (Jul 13 2020 at 20:09):

It seems to me that the definitions of update_row and update_column in linear_algebra/nonsingular_inverse are swapped. If I have

import data.matrix.notation
import linear_algebra.nonsingular_inverse

example (a b c d : ℕ) (A : matrix (fin 2) (fin 2) ℕ) (hA : A = ![![a, b], ![c, d]]) :
A 1 0 = c := by simp [hA]


then I would expect the following to be true:

example (a b c d : ℕ) (A : matrix (fin 2) (fin 2) ℕ) (hA : A = ![![a, b], ![c, d]]) :
update_row A 0 (λ i, a) 1 0 = c := by simp [hA]


example (a b c d : ℕ) (A : matrix (fin 2) (fin 2) ℕ) (hA : A = ![![a, b], ![c, d]]) :
update_row A 0 (λ i, a) 1 0 = a := by simp [hA]


#### Anne Baanen (Jul 13 2020 at 20:17):

Definitely my fault, I'm rubbish at remembering which index is for a row or a column

#### Yakov Pechersky (Jul 13 2020 at 20:18):

No worries! Was just trying to make lemmas for data.matrix.notation following your suggestion about using cramer_map for derivative definitions.

#### Yakov Pechersky (Jul 13 2020 at 20:19):

A non-Cramer definition, using Laplace:

def det' {R : Type*} [field R] :
Π {n : ℕ}, matrix (fin n) (fin n) R -> fin n -> R
| 0 _ _ := 1
| (n + 1) M i :=
match i with
| ⟨0, _⟩  := ∑ j, (M i j * (-1 : R) ^ (i.val + j.val) * det' (minor M (fin.succ_above i) (fin.succ_above j)) 0)
| ⟨k + 1, hk⟩ := ∑ j, (M i j * (-1 : R) ^ (i.val + j.val) * det' (minor M (fin.succ_above i) (fin.succ_above j))