## 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):

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