add_left_cancel_monoid

Stream: Is there code for X?

[Sebastien Gouezel]

I can't find the name of the structure in which addition is left-cancellative, like add_left_cancel_semigroup, but with a zero that plays well with the addition, like in an add_monoid. My natural guess would be add_left_cancel_monoid, but this doesn't exist. I just want to cover ℕ and groups, in fact, so any typeclass containing the two and with the two above properties would be enough for me.

By the way, this kind of question would not make sense with a structure like the one for topological spaces, with a rather small spine with the main players, and mixins to add all kinds of properties. I wish the algebraic hierarchy would also be like this...

[Mario Carneiro]

Why not just define it? It's not difficult and you get all the theorems for free

[Mario Carneiro]

class add_left_cancel_monoid A extends add_left_cancel_semigroup A, add_monoid A

add instances for groups and nat and you are ready to go

[Sebastien Gouezel]

Sure, but then I will also need to add an instance for nnreal, and maybe some other guy I am not thinking of.

[Mario Carneiro]

only if you need it

[Sebastien Gouezel]

With mixins, there would be no need to define a new class.

[Mario Carneiro]

I'm not convinced that this is actually saving much in this instance

[Mario Carneiro]

what I described seems pretty easy

[Sebastien Gouezel]

And the natural place for it is in core...

[Mario Carneiro]

No, you can do that anywhere

[Mario Carneiro]

there is no requirement that this be in core

[Mario Carneiro]

mathlib does this in a few places, inserting new classes in the middle of the hierarchy

[Sebastien Gouezel]

Sure, I am just saying that the natural place is in core, in init/algebra/groups.lean, close to add_monoid and add_left_cancel_semigroup.

[Mario Carneiro]

maybe, but that isn't a reason to complain about it, that's an organizational decision

[Mario Carneiro]

Actually it seems that the winds are blowing to take more of the algebraic hierarchy out of core anyway

[Mario Carneiro]

I don't want to be dismissive about mixins, but it is a complicated issue that affects many things and I think that any reinvestigation should be carefully thought out; single examples aren't enough unless the difference is really stark