no goals
l : Type ?u.381155
m : Type u_1
n : Type u_2
o : Type u_3
m' : o → Type ?u.381169
n' : o → Type ?u.381174
R : Type ?u.381177
S : Type ?u.381180
α : Type v
β : Type w
γ : Type ?u.381187
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M M' : Matrix m n α
N : Matrix n o α
⊢ (M - M') ⬝ N = M ⬝ N - M' ⬝ N
rw [sub_eq_add_neg, Matrix.add_mul, Matrix.neg_mul, sub_eq_add_neg]