Learning class declaration

Stream: new members

[Luiz Kazuo Takei]

I am trying to learn about class declaration and tried to define an Abelian group like this:

class AbGroup (G : Type) extends HMul G G G, Inv G, One G where
  mul_assoc : ∀ x y z, x * y * z = x * (y * z)
  one_mul : ∀ x, 1 * x = x
  mul_inv : ∀ x, x * x⁻¹ = 1
  mul_comm : ∀ x y, x * y = y * x

In the mul_assoc type, I get an error message saying

typeclass instance problem is stuck, it is often due to metavariables
HMul ?m.31 (?m.39 x y z) (?m.35 x y z)

Could anyone help me understand why?

[Ruben Van de Velde]

Does it work with ∀ x y z : G, ...?

[Luiz Kazuo Takei]

Yes, it does! Thanks!

[Luiz Kazuo Takei]

By the way, I read somewhere that I should avoid using the class Mul and instead use HMul. Is this correct?

[Ruben Van de Velde]

I'm not sure I'd agree with that

[Ruben Van de Velde]

But perhaps it was in a context where this was relevant

[Luiz Kazuo Takei]

It must be an AI hallucination then... :P I believe it even said that Mul was deprecated and was there only to be compatible with Lean 3.

Thanks for clarifying it.

[Kevin Buzzard]

docs#Group

[Kevin Buzzard]

docs#Semigroup

[Kevin Buzzard]

Yeah mathlib's Group extends Semigroup (via Monoid etc) and Semigroup uses Mul.