case nil
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.115849
inst✝⁵ : Field 𝕜
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
i j : n
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
⊢ List.prod (List.map (toMatrix ∘ reindexEquiv e) []) = ↑(reindexAlgEquiv R e) (List.prod (List.map toMatrix []))

case cons
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.115849
inst✝⁵ : Field 𝕜
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
i j : n
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : List.prod (List.map (toMatrix ∘ reindexEquiv e) L) = ↑(reindexAlgEquiv R e) (List.prod (List.map toMatrix L))
⊢ List.prod (List.map (toMatrix ∘ reindexEquiv e) (t :: L)) =
    ↑(reindexAlgEquiv R e) (List.prod (List.map toMatrix (t :: L)))
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.115849
inst✝⁵ : Field 𝕜
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
i j : n
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
L : List (TransvectionStruct n R)
⊢ List.prod (List.map (toMatrix ∘ reindexEquiv e) L) = ↑(reindexAlgEquiv R e) (List.prod (List.map toMatrix L))
induction' L with t L IH
no goals
case nil
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.115849
inst✝⁵ : Field 𝕜
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
i j : n
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
⊢ List.prod (List.map (toMatrix ∘ reindexEquiv e) []) = ↑(reindexAlgEquiv R e) (List.prod (List.map toMatrix []))
simp
case cons
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.115849
inst✝⁵ : Field 𝕜
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
i j : n
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : List.prod (List.map (toMatrix ∘ reindexEquiv e) L) = ↑(reindexAlgEquiv R e) (List.prod (List.map toMatrix L))
⊢ ↑(reindex e e) (toMatrix t) ⬝ ↑(reindex e e) (List.prod (List.map toMatrix L)) =
    ↑(reindex e e) (toMatrix t ⬝ List.prod (List.map toMatrix L))
case cons
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.115849
inst✝⁵ : Field 𝕜
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
i j : n
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : List.prod (List.map (toMatrix ∘ reindexEquiv e) L) = ↑(reindexAlgEquiv R e) (List.prod (List.map toMatrix L))
⊢ List.prod (List.map (toMatrix ∘ reindexEquiv e) (t :: L)) =
    ↑(reindexAlgEquiv R e) (List.prod (List.map toMatrix (t :: L)))
simp only [toMatrix_reindexEquiv, IH, Function.comp_apply, List.prod_cons, mul_eq_mul,
  reindexAlgEquiv_apply, List.map]
no goals
case cons
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.115849
inst✝⁵ : Field 𝕜
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
i j : n
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : List.prod (List.map (toMatrix ∘ reindexEquiv e) L) = ↑(reindexAlgEquiv R e) (List.prod (List.map toMatrix L))
⊢ ↑(reindex e e) (toMatrix t) ⬝ ↑(reindex e e) (List.prod (List.map toMatrix L)) =
    ↑(reindex e e) (toMatrix t ⬝ List.prod (List.map toMatrix L))
exact (reindexAlgEquiv_mul _ _ _ _).symm