Zulip Chat Archive

Stream: Is there code for X?

Topic: smul_comm

view this post on Zulip 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