Zulip Chat Archive

Stream: new members

Topic: update_row and update_column


view this post on Zulip 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]

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]

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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))
      k, (add_lt_add_iff_right 1).mp hk
      )
  end

view this post on Zulip Yakov Pechersky (Jul 13 2020 at 20:19):

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


Last updated: May 18 2021 at 17:44 UTC