CommGroup from CommGroupWithZero

Stream: mathlib4

[Matthew Ballard]

Does this really fail?

import Mathlib

variable {α : Type*} [CommGroupWithZero α]

#synth CommGroup α

[Jireh Loreaux]

Sure? zero is not invertible.

[Matthew Ballard]

Oh duh!

[Johan Commelin]

I wish we had a better name for this concept

[Johan Commelin]

This is just the miserable name that I came up with when we needed this in the perfectoid project

[Damiano Testa]

If #synth said "could not find an inverse for zero", everything would be clearer...

[Thomas Murrills]

Johan Commelin said:

I wish we had a better name for this concept

I feel like this is pretty descriptive as names go! I guess the problem is that With connotes that what you have is still a CommGroup. Maybe a different word would show that its nature is potentially altered, e.g. something in the spirit of CommGroupAdjoinZero.

[Eric Wieser]

With is perfect terminology insofar as CommGroup G implies CommGroupWithZero (WithZero G)

[Jireh Loreaux]

personally, I think this name is fine.

[Johan Commelin]

We also have AddMonoidWithOne, and that one does imply AddMonoid...

[Johan Commelin]

And AddMonoid M does not imply AddMonoidWithOne (WithOne M) afaict

[Damiano Testa]

CommGroupButWithZero :smile:

[Ruben Van de Velde]

NotCommGroupWithZero?

[Damiano Testa]

Where are the parentheses in NotCommGroupWithZero? :smile:

[Edward van de Meent]

CommRingWithoutAdd

[Damiano Testa]

As much as I am amused by the suggestions, I think that the names GroupWithZero and MonoidWithZero are fine, actually, even though they use "different" meanings of "with".

[Matthew Ballard]

NB: my brain was turned off when I started this thread.

[Damiano Testa]

Matthew Ballard said:

NB: my brain was turned off when I started this thread.

That's how I feel in most threads.

[Eric Wieser]

C0mmGr0up / AddMono1d could replace CommGroupWithZero / AddMonoidWithOne

[Kevin Buzzard]

Matthew Ballard said:

NB: my brain was turned off when I started this thread.

I remember when I had three kids including a 3-week-old too:-)