Two ways of defining an idempotent semigroup

Stream: mathlib4

[Pieter Cuijpers]

I want to define an idempotent semigroup and now see two options:

class IdemSemigroup (G : Type*) extends Semigroup, Std.IdempotentOp toMul.mul

versus spelling it out

class IdemSemigroup (G : Type*) extends Semigroup where
   protected idempotent :  \forall a : G, a * a = a

I noticed that for a commutative semigroup (or rather Magma) it was spelled out, but don't know which is generally preferable/better style?

[Yaël Dillies]

It's better spelled out because:

1. It lets you name the field. In particular, if you wanted to eg reason about rings whose addition and multiplication are idempotent, then you couldn't do extends Ring, Std.IdempotentOp (· * ·), Std.IdempotentOp (· + ·) because that would result in a duplicated field name.
2. It lets your users not worry about what Std.IdempotentOp toMul.mul means

[Eric Wieser]

protected idempotent : Std.IdempotentOp (· * ·) woula also be a possible compromise

[Eric Wieser]

But realistically you should just add instance [IdemSemigroup G] : Std.IdempotentOp (· * ·), and everything else is probably user-hostile

[Pieter Cuijpers]

Eric Wieser said:

But realistically you should just add instance [IdemSemigroup G] : Std.IdempotentOp (· * ·), and everything else is probably user-hostile

And is this also what is generally done in Mathlib?
I mean, as soon as you realize an operator op has a property, would you always instantiate it as a Std.Property op if available? I cannot find this for CommMagma for example, but maybe I'm not looking in the right place.

[Yaël Dillies]

We rarely use the Std.Property typeclasses in mathlib

[Eric Wieser]

I think a PR to add such missing instances would be accepted though

[Eric Wieser]

But it would be for convenience with interacting with Lean core, not so much for the benefit of mathlib

[Pieter Cuijpers]

I would think Std.Property definitions are there to standardize the kind of names we give to properties, and that consistently referring back to them would make searching / automating proofs easier ultimately. But perhaps that is not what happens in practice? How are these definitions used?

[Yaël Dillies]

The Std in their name doesn't mean "standardize" but refers to Std, the core Lean library