English
Multiplying on the left by the product of SumInl-embedded transvections commutes with forming a block matrix from M and N, i.e., the product distributes as fromBlocks of the product and blocks.
Русский
Произведение слева от блокированной матрицы эквивалентно блочно-диагональному разложению с учетом суммирования SumInl.
LaTeX
$$$\\Big(\\prod (toMatrix \\circ sumInl p)\\Big) \\cdot \\operatorname{fromBlocks}(M,0,0,N) = \\operatorname{fromBlocks}\\Big((\\prod toMatrix \\circ sumInl p)\\,M,0,0,N\\Big)$$$
Lean4
@[simp]
theorem sumInl_toMatrix_prod_mul [Fintype n] [Fintype p] (M : Matrix n n R) (L : List (TransvectionStruct n R))
(N : Matrix p p R) :
(L.map (toMatrix ∘ sumInl p)).prod * fromBlocks M 0 0 N = fromBlocks ((L.map toMatrix).prod * M) 0 0 N := by
induction L with
| nil => simp
| cons t L IH => simp [Matrix.mul_assoc, IH, toMatrix_sumInl, fromBlocks_multiply]
