English
If L is a list of TransvectionStruct, then the product of the reindexed matrices equals the image under reindexAlgEquiv of the product of the original matrices.
Русский
Если L — список TransvectionStruct, то произведение перенормированных матриц равно образу по reindexAlgEquiv от произведения исходных матриц.
LaTeX
$$$\\prod (toMatrix \\circ reindexEquiv e)\\;L = \\operatorname{reindexAlgEquiv}(R)\\;\\_\\;e\\; \\Big(\\prod toMatrix L\\Big)$$$
Lean4
theorem toMatrix_reindexEquiv_prod (e : n ≃ p) (L : List (TransvectionStruct n R)) :
(L.map (toMatrix ∘ reindexEquiv e)).prod = reindexAlgEquiv R _ e (L.map toMatrix).prod := by
induction L with
| nil => simp
| cons t L
IH =>
simp only [toMatrix_reindexEquiv, IH, Function.comp_apply, List.prod_cons, reindexAlgEquiv_apply, List.map]
exact (reindexAlgEquiv_mul R _ _ _ _).symm