Theorems · Theorem · linear algebra

Matrix.fromBlocks_multiply

∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {p : Type u_5} {q : Type u_6} {α : Type u_12}
  [inst : Fintype l] [inst_1 : Fintype m] [inst_2 : NonUnitalNonAssocSemiring α] (A : Matrix n l α) (B : Matrix n m α)
  (C : Matrix o l α) (D : Matrix o m α) (A' : Matrix l p α) (B' : Matrix l q α) (C' : Matrix m p α) (D' : Matrix m q α),
  Matrix.fromBlocks A B C D * Matrix.fromBlocks A' B' C' D' =
    Matrix.fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D')

Defined in

Mathlib.Data.Matrix.Block

Cited by

12 results in Mathlib

Foundations

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

Assumes

FintypeFintypeNonUnitalNonAssocSemiring