Theorems · Theorem · linear algebra

Matrix.toBlock_mul_eq_mul

∀ {R : Type u_10} [inst : CommRing R] {m : Type u_14} {n : Type u_15} {k : Type u_16} [inst_1 : Fintype n]
  (p : m → Prop) (q : k → Prop) (A : Matrix m n R) (B : Matrix n k R),
  (A * B).toBlock p q = A.toBlock p ⊤ * B.toBlock ⊤ q

Defined in

Mathlib.Data.Matrix.Block

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingFintype