mul_left_cancel' for modules

Stream: Is there code for X?

[Scott Morrison]

Where do I find the module version of src#mul_left_cancel'?

[Scott Morrison]

I would be happy with something like

lemma smul_left_cancel {α β} [field α] [add_comm_monoid β] [semimodule α β]
  (a : α) (h : a ≠ 0) (m n : β) (h : a • m = a • n) : m = n :=

[Yury G. Kudryashov]

I'm afraid that we don't have this. You might want to use docs#smul_eq_zero in the proof.

[Adam Topaz]

There's also src#mul_action.eq_inv_smul_iff for mul_action by a group, which doesn't seem to have an analogue for scalar multiplication by a division ring.

[Yury G. Kudryashov]

I wonder why we don't use the corresponding equiv lemma in the proof.