decide
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
h10 : Fin.succAbove 1 0 = 0
h11 : Fin.succAbove 1 1 = 2
h12 : Fin.succAbove 1 2 = 3
h20 : Fin.succAbove 2 0 = 0
h21 : Fin.succAbove 2 1 = 1
h22 : Fin.succAbove 2 2 = 3
h30 : Fin.succAbove 3 0 = 0
h31 : Fin.succAbove 3 1 = 1
h32 : Fin.succAbove 3 2 = 2
s0 : Fin.succ 0 = 1
s1 : Fin.succ 1 = 2
s2 : Fin.succ 2 = 3
a0 : (-1) ^ ↑0 = 1
a1 : (-1) ^ ↑1 = -1
a2 : (-1) ^ ↑2 = 1
⊢ Odd ↑3
no goals