∀ {R₁ : Type u_7} {S₁ : Type u_6} {R₂ : Type u_5} {S₂ : Type u_4} {N₂ : Type u_1} {n : Type u_2} {m : Type u_3}
  [inst : Semiring R₁] [inst_1 : Semiring S₁] [inst_2 : Semiring R₂] [inst_3 : Semiring S₂] [inst_4 : AddCommMonoid N₂]
  [inst_5 : Module S₁ N₂] [inst_6 : Module S₂ N₂] [inst_7 : Fintype n] [inst_8 : Fintype m] (σ₁ : R₁ →+* S₁)
  (σ₂ : R₂ →+* S₂) (f : Matrix n m N₂) (x : R₂) (v : n → R₁) (w : m → R₂),
  (fun v w => ∑ i, ∑ j, σ₂ (w j) • σ₁ (v i) • f i j) v (x • w) =
    σ₂ x • (fun v w => ∑ i, ∑ j, σ₂ (w j) • σ₁ (v i) • f i j) v w