Zulip Chat Archive
Stream: general
Topic: weird structure
Kenny Lau (Jan 30 2019 at 20:26):
What's a structure that is add_comm_monoid + semigroup + mul_zero_class + distrib?
Kenny Lau (Jan 30 2019 at 20:26):
or, is there a better grouping?
Reid Barton (Jan 30 2019 at 20:40):
is that a noncommutative nonunital ring?
Kenny Lau (Jan 30 2019 at 20:40):
That would be a rng
Kenny Lau (Jan 30 2019 at 20:40):
but it's not in mathlib yet
Kenny Lau (Jan 30 2019 at 20:41):
so in the meantime is there a better grouping using what is currently available?
Last updated: Dec 20 2023 at 11:08 UTC