n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type ?u.737904
inst✝ : CommRing S
A : SL(2, R)
⊢ vecCons ![↑A 1 1, -↑A 0 1] ![![-↑A 1 0, ↑A 0 0]] 1 1 * vecCons ![↑A 1 1, -↑A 0 1] ![![-↑A 1 0, ↑A 0 0]] 0 0 -
      vecCons ![↑A 1 1, -↑A 0 1] ![![-↑A 1 0, ↑A 0 0]] 0 1 * vecCons ![↑A 1 1, -↑A 0 1] ![![-↑A 1 0, ↑A 0 0]] 1 0 =
    1
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type ?u.737904
inst✝ : CommRing S
A : SL(2, R)
⊢ det ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] = 1
rw [Matrix.det_fin_two, mul_comm]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type ?u.737904
inst✝ : CommRing S
A : SL(2, R)
⊢ ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type ?u.737904
inst✝ : CommRing S
A : SL(2, R)
⊢ vecCons ![↑A 1 1, -↑A 0 1] ![![-↑A 1 0, ↑A 0 0]] 1 1 * vecCons ![↑A 1 1, -↑A 0 1] ![![-↑A 1 0, ↑A 0 0]] 0 0 -
      vecCons ![↑A 1 1, -↑A 0 1] ![![-↑A 1 0, ↑A 0 0]] 0 1 * vecCons ![↑A 1 1, -↑A 0 1] ![![-↑A 1 0, ↑A 0 0]] 1 0 =
    1
simp only [cons_val_zero, cons_val_one, head_cons, mul_neg, neg_mul, neg_neg]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type ?u.737904
inst✝ : CommRing S
A : SL(2, R)
this : det ↑A = 1
⊢ ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type ?u.737904
inst✝ : CommRing S
A : SL(2, R)
⊢ ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
have := A.2
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type ?u.737904
inst✝ : CommRing S
A : SL(2, R)
this : ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
⊢ ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type ?u.737904
inst✝ : CommRing S
A : SL(2, R)
this : det ↑A = 1
⊢ ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
rw [Matrix.det_fin_two] at this
no goals
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type ?u.737904
inst✝ : CommRing S
A : SL(2, R)
this : ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
⊢ ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
convert this