isAddCommGroup field in ModuleCat

Stream: mathlib4

[Kevin Buzzard]

Mathlib has this

structure ModuleCat where
  private mk ::
  /-- the underlying type of an object in `ModuleCat R` -/
  carrier : Type v
  [isAddCommGroup : AddCommGroup carrier]
  [isModule : Module R carrier]

Why isAddCommGroup? Shouldn't this be toAddCommGroup? Or even addCommGroup? Similarly for isModule.

[Eric Wieser]

instance X.toY I believe should only be used when X itself is a typeclass

[Yaël Dillies]

I would go for addCommGroup