Zulip Chat Archive

Stream: maths

Topic: ring.inverse

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?

Yury G. Kudryashov (Oct 05 2020 at 07:00):

@Heather Macbeth @Johan Commelin

Johan Commelin (Oct 05 2020 at 07:01):

Do you even need the zero?

Johan Commelin (Oct 05 2020 at 07:02):

Can't you just do this for any monoid?

Yury G. Kudryashov (Oct 05 2020 at 07:09):

It's zero for non-invertible elements.

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.

Johan Commelin (Oct 05 2020 at 07:14):

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

Johan Commelin (Oct 05 2020 at 07:15):

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

Heather Macbeth (Oct 05 2020 at 12:24):

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

Heather Macbeth (Oct 05 2020 at 12:25):

Note that it will probably conflict with #4407.

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.

Eric Wieser (Oct 26 2021 at 00:05):

Do we still want to rename this? The generalization was made without a rename in #6603

Yury G. Kudryashov (Oct 26 2021 at 06:54):

I don't care about the name.

Last updated: Dec 20 2023 at 11:08 UTC