A submonoid of a `cancel_monoid_with_zero` also cancels

Stream: Is there code for X?

[Anne Baanen]

I saw that @Yakov Pechersky did some work on cancel_monoids_with_zero, so is a version of function.injective.cancel_comm_monoid_wiith_zero analogous to docs#function.injective.cancel_comm_monoid available in an unmerged branch, or shall I add it myself?

[Anne Baanen]

Nevermind, found docs#function.injective.cancel_monoid_with_zero which is enough for my purposes.

[Eric Wieser]

We should probably have the version you mention even if you don't really need it

[Anne Baanen]

Added in #8515 :+1: