smul_comm

Stream: Is there code for X?

[Oliver Nash]

I'm a little surprised I can't find the following:

universes u v

lemma smul_comm {R : Type u} {M : Type v}
  [comm_ring R] [add_comm_group M] [module R M] (c₁ c₂ : R) (m : M) :
  c₁ • c₂ • m = c₂ • c₁ • m := by rw [←mul_smul, ←mul_smul, mul_comm] -- library_search fails

Can it really be missing?