Zulip Chat Archive

Stream: maths

Topic: ring.inverse


view this post on Zulip Yury G. Kudryashov (Oct 05 2020 at 07:00):

I'd like to redefine docs#ring.inverse for a docs#monoid_with_zero instead of a ring (why not?). Probably this means that it should be renamed. What name would you suggest? inverse₀? Something better?

view this post on Zulip Yury G. Kudryashov (Oct 05 2020 at 07:00):

@Heather Macbeth @Johan Commelin

view this post on Zulip Johan Commelin (Oct 05 2020 at 07:01):

Do you even need the zero?

view this post on Zulip Johan Commelin (Oct 05 2020 at 07:02):

Can't you just do this for any monoid?

view this post on Zulip Yury G. Kudryashov (Oct 05 2020 at 07:09):

It's zero for non-invertible elements.

view this post on Zulip Yury G. Kudryashov (Oct 05 2020 at 07:11):

I can redefine it to be 1 in this case. Then it won't agree with has_inv.inv for fields but this should not be too important.

view this post on Zulip Johan Commelin (Oct 05 2020 at 07:14):

Yeah... I can understand that 0 might be convenient

view this post on Zulip Johan Commelin (Oct 05 2020 at 07:15):

I would abbreviate it to inv\0 if you choose the monoid_with_zero route

view this post on Zulip Heather Macbeth (Oct 05 2020 at 12:24):

No objections. I like inverse₀ or inv₀. Do you have a use in mind?

view this post on Zulip Heather Macbeth (Oct 05 2020 at 12:25):

Note that it will probably conflict with #4407.

view this post on Zulip Yury G. Kudryashov (Oct 05 2020 at 13:25):

I just wanted to apply results about ring.inverse to the usual division, and noticed that the definition doesn't use addition.


Last updated: May 06 2021 at 19:30 UTC