## Stream: Is there code for X?

### Topic: smul_comm

#### Oliver Nash (Feb 10 2020 at 18:59):

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?

Last updated: May 17 2021 at 15:13 UTC