Zulip Chat Archive
Stream: general
Topic: has_dvd
Johan Commelin (May 11 2020 at 17:59):
In core, you can deduce has_dvd automatically from comm_semiring. Do we want to change that to simply has_mul?
Chris Hughes (May 11 2020 at 18:01):
We might want commutativity as well.
Chris Hughes (May 11 2020 at 18:01):
Otherwise there's left and right divisibility.
Johan Commelin (May 11 2020 at 18:03):
Ok, so comm_semigroup.
Alex J. Best (May 11 2020 at 18:56):
I've also wanted this recently! I think there are a few instances that can be removed with this definition, for pnat for instance.
Last updated: Dec 20 2023 at 11:08 UTC