Theorems · Theorem · linear algebra

Matrix.toBlock_mul_eq_add

∀ {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 : n → Prop) [inst_2 : DecidablePred q] (r : k → Prop) (A : Matrix m n R) (B : Matrix n k R),
  (A * B).toBlock p r = A.toBlock p q * B.toBlock q r + (A.toBlock p fun i => ¬q i) * B.toBlock (fun i => ¬q i) r

Defined in

Mathlib.Data.Matrix.Block

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingFintypeDecidablePred