(Has)InvolutiveInv

Stream: mathlib4

[Kevin Buzzard]

In Mathlib4 Algebra.Group.Defs we have

/-- Auxiliary typeclass for types with an involutive `Neg`. -/
class HasInvolutiveNeg (A : Type _) extends Neg A where
  neg_neg : ∀ x : A, - -x = x

/-- Auxiliary typeclass for types with an involutive `Inv`. -/
@[to_additive]
class HasInvolutiveInv (G : Type _) extends Inv G where
  inv_inv : ∀ x : G, x⁻¹⁻¹ = x

Should those be InvolutiveNeg and InvolutiveInv?

[Ruben Van de Velde]

I suspect yes

[Jireh Loreaux]

Yes, definitely. Just haven't gotten around to changing them yet.

[Kevin Buzzard]

I can just do them now; I'm doing groupy stuff.

[Ruben Van de Velde]

Looks like mathlib4#832 is attempting the rename as well

[Kevin Buzzard]

oh good catch -- thanks!

[Wojciech Nawrocki]

I looked around and also found other uses of Has but didn't go for a more global refactor because for some it is not very clear what the new name should be - e.g. HasQuotient would conflict with Quotient.

[Scott Morrison]

I think HasQuotient is okay.

[Scott Morrison]

It's a slightly stronger sense of 'has' here. :-)