Semigroup.to_isAssociative

Stream: mathlib4

[Kevin Buzzard]

The mathlib4 port of Algebra.Group.Defs is missing

@[to_additive]
instance Semigroup.to_isAssociative [Semigroup G] : IsAssociative G (· * ·) :=
⟨mul_assoc⟩

Is this because it's a bad instance or just because it was missed for some reason? I've added it to the file.

[Kevin Buzzard]

mathlib4#826 in case it should be added

[Yaël Dillies]

Oh sorry I changed it in mathlib very recently.

[Kevin Buzzard]

oh! You edited a frozen mathlib3 file without making the mathlib4 PR? I just found

@[to_additive]
instance CommSemigroup.to_isCommutative : IsCommutative G (· * ·) :=
  ⟨mul_comm⟩
#align comm_semigroup.to_is_commutative CommSemigroup.to_isCommutative

too. Is there anything else?

[Jireh Loreaux]

port status should have picked up on this ... ?

[Kevin Buzzard]

I'm not entirely sure how to proceed here. Merging the mathlib4 PR will just add to the confusion.

[Kevin Buzzard]

Given that I need the instance I may as well just attempt to port the PR right now.

[Kevin Buzzard]

I am now totally confused. The file was edited 8 days ago but by Riccardo not Yael, and Riccardo made a corresponding mathlib4 PR.

[Kevin Buzzard]

Yael, the missing instance was added by Yury three years ago. So my question comes back to "is there a reason why instance semigroup.to_is_associative [semigroup G] : is_associative G (*) := and instance comm_semigroup.to_is_commutative [comm_semigroup G] : is_commutative G (*) := were not ported to mathlib4? Are they bad instances or were they just missed for some random reason?