# Zulip Chat Archive

## 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.cons`

as well

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

Are you always adding on an edge, or inserting?

Last updated: Dec 20 2023 at 11:08 UTC