toMatrix_reindexEquiv_prod — Mathlib

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

Похожие утверждения