Theorems · Theorem · linear algebra

dotProduct_smul

∀ {m : Type u_2} {R : Type u_7} {α : Type v} [inst : Fintype m] [inst_1 : Mul α] [inst_2 : AddCommMonoid α]
  [inst_3 : DistribSMul R α] [SMulCommClass R α α] (x : R) (v w : m → α), v ⬝ᵥ x • w = x • (v ⬝ᵥ w)

Defined in

Mathlib.Data.Matrix.Mul

Cited by

4 results in Mathlib

Foundations

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

Assumes

FintypeMulAddCommMonoidDistribSMulSMulCommClass