## Stream: new members

### Topic: extracting entries from matrices

#### Apurva Nakade (Jul 23 2020 at 13:15):

Given a matrix A, I want to define a new matrix obtained by adding a row and column to A.
I tried the following but it fails because of type mismatch. Dunno how to fix it.

import data.fintype.basic
import data.matrix.basic

open_locale matrix

def matrix_extension {k : ℕ} (A : matrix (fin k) (fin k) ℕ) : matrix (fin (k+1)) (fin (k+1)) ℕ
:=
λ i j,
match i.val, j.val with
| 0, 0     := 1
| 0, _     := 0
| _, 0     := 0
| (x+1), (y+1) := A x y
end


#### Apurva Nakade (Jul 23 2020 at 13:16):

A x y doesn't work because A is expecting a pair of fintype

#### Jalex Stark (Jul 23 2020 at 13:17):

I think A is expecting a pair of fin k

#### Jalex Stark (Jul 23 2020 at 13:17):

does something like A ⟨x, _ ⟩ ⟨y, _⟩ work?

#### Anne Baanen (Jul 23 2020 at 13:18):

Instead of writing a match statement, you can also try fin.cons : α -> (fin n -> α) -> fin (n+1) -> α.

#### Apurva Nakade (Jul 23 2020 at 13:18):

Jalex Stark said:
It says don't know how to synthesize placeholder
context:

#### Markus Himmel (Jul 23 2020 at 13:20):

Here is one way to do it using a match, but @Anne Baanen's way is almost certainly better.

import data.fintype.basic
import data.matrix.basic

open_locale matrix

def matrix_extension {k : ℕ} (A : matrix (fin k) (fin k) ℕ) : matrix (fin (k+1)) (fin (k+1)) ℕ
:=
λ i j,
match i, j with
| ⟨0, _⟩, ⟨0, _⟩       := 1
| ⟨0, _⟩, _            := 0
| _, ⟨0, _⟩            := 0
| ⟨x+1, hx⟩, ⟨y+1, hy⟩ := A ⟨x, nat.lt_of_succ_lt_succ hx⟩ ⟨y, nat.lt_of_succ_lt_succ hy⟩
end


#### Apurva Nakade (Jul 23 2020 at 13:24):

Thank you!!!

This definitely works, with the added bonus that I understand what's going on :P
I will give it a try using fin.consas well

#### Yakov Pechersky (Jul 23 2020 at 13:43):

Are you always adding on an edge, or inserting?

Last updated: May 14 2021 at 23:14 UTC