Theorems · Theorem

Matrix.cons_mul

∀ {α : Type u} {m : ℕ} {n' : Type uₙ} {o' : Type uₒ} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n']
  (v : n' → α) (A : Fin m → n' → α) (B : Matrix n' o' α),
  Matrix.of (Matrix.vecCons v A) * B = Matrix.of (Matrix.vecCons (Matrix.vecMul v B) (Matrix.of.symm (Matrix.of A * B)))

Defined in

Mathlib.LinearAlgebra.Matrix.Notation

Cited by

8 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext, Quot.sound

Assumes

NonUnitalNonAssocSemiringFintype