I have a `'a::{factorial_semiring, comm_ring}`

. I would like to derive the `semiring_modulo`

class for it, by defining `a mod b = a - a div b`

. Is this possible?

Not generically, no. But you can probably do it for a particular instance.

Our of curiosity, what type is it that you have?

I just want to prove some theorems for an arbitrary UFD

Yeah then you probably have to assume a type class that has modulo if you want modulo to be available.

The only other way I can think of is to define a type `'a ufdmod`

that is basically a copy of `'a`

except that it also has a modulo operation defined the way you just said.

Then you can pull all the results that don't use `mod`

over from `'a ufdmod`

to `'a`

using e.g. the transfer tool.

Might not be worth it though.

Might be easier to just not use `mod`

.

What you *could* also do is interpret the `semiring_modulo`

locale with that particular definition of `mod`

.

I've done that sort of thing before. It's a little bit messy, but it does the job.

Last updated: Sep 25 2022 at 23:25 UTC