mul_sumInl_toMatrix_prod — Mathlib

English

Multiplication on the right by the block-matrix fromBlocks M 0 0 N corresponds to multiplying the left-by-sumInl product on the transvection matrices.

Русский

Умножение справа на блочно-диагональную матрицу соответствует умножению слева на произведение трансвеκций SumInl.

LaTeX

$$$\\operatorname{fromBlocks}(M,0,0,N) \\cdot (\\text{map } toMatrix \\circ sumInl p)\\!\\text{prod} = \\operatorname{fromBlocks}\\Big(M \\cdot (\\text{map } toMatrix \\circ sumInl p)\\!,0,0,N\\Big)$$$

Lean4

@[simp]
theorem mul_sumInl_toMatrix_prod [Fintype n] [Fintype p] (M : Matrix n n R) (L : List (TransvectionStruct n R))
    (N : Matrix p p R) :
    fromBlocks M 0 0 N * (L.map (toMatrix ∘ sumInl p)).prod = fromBlocks (M * (L.map toMatrix).prod) 0 0 N := by
  induction L generalizing M N with
  | nil => simp
  | cons t L IH => simp [IH, toMatrix_sumInl, fromBlocks_multiply]

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