l : Type u_2
R : Type u_1
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ (-1) ^ (Fintype.card l + Fintype.card l) = 1
l : Type u_2
R : Type u_1
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ det (J l R) * det (J l R) = 1
rw [← det_mul, J_squared, ← one_smul R (-1 : Matrix _ _ R), smul_neg, ← neg_smul, det_smul,
  Fintype.card_sum, det_one, mul_one]
case h
l : Type u_2
R : Type u_1
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ Even (Fintype.card l + Fintype.card l)
l : Type u_2
R : Type u_1
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ (-1) ^ (Fintype.card l + Fintype.card l) = 1
apply Even.neg_one_pow
no goals
case h
l : Type u_2
R : Type u_1
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ Even (Fintype.card l + Fintype.card l)
exact even_add_self _