# Zulip Chat Archive

## Stream: new members

### Topic: begginer matrix question

#### Chris Birkbeck (Apr 06 2021 at 09:56):

Hello, I'm new here and have been playing around with matrices in Lean. First of all, sorry if this is not the correct stream to ask this in.

My problems are essentially with matrix coercion. I’ve seen that we there is the following notation for matrices and I would like to know how to use it for special_linear_group. Specifically, how do I take

```
import linear_algebra.matrix
import data.matrix.notation
def N : matrix (fin 2) (fin 2 ) ℤ:= ![![-1, 0], ![0, -1]]
```

and turn it into an element of

```
import linear_algebra.special_linear_group
def SL2Z := special_linear_group (fin 2) ℤ
```

I assume this wont be automatic as one has prove N has determinant 1, but I dont know how to get lean to take a 2x2 matrix of determinant 1 and think of it as an element of SL2Z.

Thank you

#### Johan Commelin (Apr 06 2021 at 10:00):

@Chris Birkbeck Welcome! This stream is fine (-;

#### Johan Commelin (Apr 06 2021 at 10:00):

You can turn a matrix into an element of `SL2Z`

using `\< _, _ \>`

. If you type that into VScode, the `\<`

and `\>`

will turn into funny unicode brackets.

#### Johan Commelin (Apr 06 2021 at 10:01):

The end result will be `\<your_matrix, proof_that_det_eq_1\>`

#### Chris Birkbeck (Apr 06 2021 at 10:10):

Ah that's what I needed. Thank you very much!

#### Johan Commelin (Apr 06 2021 at 10:13):

I guess the following also works:

```
def my_matrix : SL2Z :=
_
```

Now put your cursor on the `_`

, and wait till a little :bulb: appears.

#### Johan Commelin (Apr 06 2021 at 10:13):

Then you can click it, or type `Ctrl`

-`.`

.

#### Johan Commelin (Apr 06 2021 at 10:14):

Now choose `generate skeleton`

(almost at the bottom of hte menu)

#### Chris Birkbeck (Apr 06 2021 at 13:25):

Thats really useful, thank you. Now, say I wanted to use this notation. I was trying to prove that N^2 is 1. I end up with something that looks like

`⟨N, proof⟩ * ⟨N, proof⟩ = 1`

Now, I can't seem to figure out how to simplify this. I guess I'm confused how one splits this into working with the matrices and proofs separetely (but maybe one doesnt want to do this and there is something better?).

#### Johan Commelin (Apr 06 2021 at 13:26):

@Chris Birkbeck So now there is hopefully an `ext`

-lemma for `SL2Z`

that says that for proving equalities it suffices to check equality of the matrices.

#### Johan Commelin (Apr 06 2021 at 13:26):

If it doesn't exist `apply subtype.coe_injective`

hopefully works. (I'm just guessing.)

#### Johan Commelin (Apr 06 2021 at 13:28):

@Chris Birkbeck You might want to just work with `special_linear_group`

, instead of making your `SL2Z`

definition on top of it.

#### Johan Commelin (Apr 06 2021 at 13:29):

Then the `ext`

tactic will help you further.

#### Johan Commelin (Apr 06 2021 at 13:29):

It will apply this lemma: https://leanprover-community.github.io/mathlib_docs/linear_algebra/special_linear_group.html#matrix.special_linear_group.ext

#### Johan Commelin (Apr 06 2021 at 13:29):

Which says that if all coefficients are equal, then you are done.

#### Johan Commelin (Apr 06 2021 at 13:30):

After `ext`

, you do `intros i j`

, and then `fin_cases i; fin_cases j`

should give you 4 goals, one for each coefficient.

#### Johan Commelin (Apr 06 2021 at 13:30):

With a bit of luck, each of them can be closed with `simp`

.

Last updated: May 16 2021 at 21:11 UTC