## Stream: Is there code for X?

### Topic: mul_left_cancel' for modules

#### Scott Morrison (Sep 30 2020 at 01:10):

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

#### Scott Morrison (Sep 30 2020 at 01:11):

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 (Sep 30 2020 at 02:11):

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

#### Adam Topaz (Sep 30 2020 at 02:36):

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 (Sep 30 2020 at 03:10):

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

Last updated: May 16 2021 at 05:21 UTC