case nil
n : Type u_1
p : Type ?u.23948
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
⊢ det (List.prod (List.map toMatrix [])) = 1

case cons
n : Type u_1
p : Type ?u.23948
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
t : TransvectionStruct n 𝕜
L : List (TransvectionStruct n 𝕜)
IH : det (List.prod (List.map toMatrix L)) = 1
⊢ det (List.prod (List.map toMatrix (t :: L))) = 1
n : Type u_1
p : Type ?u.23948
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
L : List (TransvectionStruct n 𝕜)
⊢ det (List.prod (List.map toMatrix L)) = 1
induction' L with t L IH
no goals
case nil
n : Type u_1
p : Type ?u.23948
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
⊢ det (List.prod (List.map toMatrix [])) = 1
simp
no goals
case cons
n : Type u_1
p : Type ?u.23948
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
t : TransvectionStruct n 𝕜
L : List (TransvectionStruct n 𝕜)
IH : det (List.prod (List.map toMatrix L)) = 1
⊢ det (List.prod (List.map toMatrix (t :: L))) = 1
simp [IH]