Zulip Chat Archive

Stream: general

Topic: weird structure


view this post on Zulip Kenny Lau (Jan 30 2019 at 20:26):

What's a structure that is add_comm_monoid + semigroup + mul_zero_class + distrib?

view this post on Zulip Kenny Lau (Jan 30 2019 at 20:26):

or, is there a better grouping?

view this post on Zulip Reid Barton (Jan 30 2019 at 20:40):

is that a noncommutative nonunital ring?

view this post on Zulip Kenny Lau (Jan 30 2019 at 20:40):

That would be a rng

view this post on Zulip Kenny Lau (Jan 30 2019 at 20:40):

but it's not in mathlib yet

view this post on Zulip Kenny Lau (Jan 30 2019 at 20:41):

so in the meantime is there a better grouping using what is currently available?


Last updated: May 14 2021 at 04:22 UTC