Theorems · Theorem · linear algebra

Matrix.TransvectionStruct.sumInl_toMatrix_prod_mul

∀ {n : Type u_1} (p : Type u_2) {R : Type u₂} [inst : DecidableEq n] [inst_1 : DecidableEq p] [inst_2 : CommRing R]
  [inst_3 : Fintype n] [inst_4 : Fintype p] (M : Matrix n n R) (L : List (Matrix.TransvectionStruct n R))
  (N : Matrix p p R),
  (List.map (Matrix.TransvectionStruct.toMatrix ∘ Matrix.TransvectionStruct.sumInl p) L).prod *
      Matrix.fromBlocks M 0 0 N =
    Matrix.fromBlocks ((List.map Matrix.TransvectionStruct.toMatrix L).prod * M) 0 0 N

Defined in

Mathlib.LinearAlgebra.Matrix.Transvection

Cited by

1 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqDecidableEqCommRingFintypeFintype