Theorems · Theorem

Matrix.mul_empty

∀ {α : Type u} {m' : Type uₘ} {n' : Type uₙ} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n']
  (A : Matrix m' n' α) (B : Matrix n' (Fin 0) α), A * B = Matrix.of fun x => ![]

Defined in

Mathlib.LinearAlgebra.Matrix.Notation

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonUnitalNonAssocSemiringFintype