Zulip Chat Archive

Stream: Is there code for X?

Topic: mul_left_cancel' for modules


view this post on Zulip Scott Morrison (Sep 30 2020 at 01:10):

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

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

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

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

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