update_row and update_column

Stream: new members

[Yakov Pechersky]

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]

but instead it is

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]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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))
      ⟨k, (add_lt_add_iff_right 1).mp hk⟩
      )
  end

[Yakov Pechersky]

But I'm having difficulties proving things with that. So I'm trying your Cramer suggestion now.