Theorems · Theorem · linear algebra

Matrix.mul_mul_right

∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : CommSemiring α] [inst_1 : Fintype n]
  (M : Matrix m n α) (N : Matrix n o α) (a : α), (M * Matrix.of fun i j => a * N i j) = a • (M * N)

Defined in

Mathlib.Data.Matrix.Mul

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringFintype