chore: upstream Inv notation typeclass (#8345)

src/Init/Notation.lean

@@ -294,6 +294,7 @@ recommended_spelling "PProd" for "×'" in [PProd, «term_×'_»]
 @[inherit_doc] infixl:65 " ++ "  => HAppend.hAppend
 @[inherit_doc] prefix:75 "-"    => Neg.neg
 @[inherit_doc] prefix:100 "~~~"  => Complement.complement
+@[inherit_doc] postfix:max "⁻¹" => Inv.inv
 
 /-!
   Remark: the infix commands above ensure a delaborator is generated for each relations.
@@ -311,6 +312,7 @@ macro_rules | `($x % $y)   => `(binop% HMod.hMod $x $y)
 macro_rules | `($x ^ $y)   => `(rightact% HPow.hPow $x $y)
 macro_rules | `($x ++ $y)  => `(binop% HAppend.hAppend $x $y)
 macro_rules | `(- $x)      => `(unop% Neg.neg $x)
+macro_rules | `($x ⁻¹)     => `(unop% Inv.inv $x)
 
 recommended_spelling "or" for "|||" in [HOr.hOr, «term_|||_»]
 recommended_spelling "xor" for "^^^" in [HXor.hXor, «term_^^^_»]

src/Init/Prelude.lean

@@ -1451,6 +1451,15 @@ class Div (α : Type u) where
   /-- `a / b` computes the result of dividing `a` by `b`. See `HDiv`. -/
   div : α → α → α
 
+/--
+The notation typeclass for inverses.
+This enables the notation `a⁻¹ : α` where `a : α`.
+-/
+class Inv (α : Type u) where
+  /-- `a⁻¹` computes the inverse of `a`.
+  The meaning of this notation is type-dependent. -/
+  inv : α → α
+
 /-- The homogeneous version of `HMod`: `a % b : α` where `a b : α`. -/
 class Mod (α : Type u) where
   /-- `a % b` computes the remainder upon dividing `a` by `b`. See `HMod`. -/

tests/lean/diamond7.lean

@@ -14,11 +14,6 @@ set_option pp.all true
 #check CommMonoid.mk
 #print CommMonoid.toCommSemigroup
 
-class Inv (α : Type u) where
-  inv : α → α
-
-postfix:100 "⁻¹" => Inv.inv
-
 class Group (α : Type u) extends Monoid α, Inv α where
   mul_left_inv (a : α) : a⁻¹ * a = 1
 

tests/lean/run/3807.lean

@@ -766,11 +766,6 @@ instance instHSMul {α β} [SMul α β] : HSMul α β β where
 
 variable {G : Type _}
 
-class Inv (α : Type u) where
-  inv : α → α
-
-postfix:max "⁻¹" => Inv.inv
-
 class Semigroup (G : Type u) extends Mul G where
   protected mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)
 

tests/lean/run/KyleAlg.lean

@@ -9,11 +9,6 @@ class Add (α : Type u) where
   add : α → α → α
 -/
 
-class Inv (α : Type u) where
-    inv : α → α
-
-postfix:max "⁻¹" => Inv.inv
-
 export One (one)
 export Zero (zero)
 

tests/lean/run/KyleAlgAbbrev.lean

@@ -9,11 +9,6 @@ class Add (α : Type u) where
   add : α → α → α
 -/
 
-class Inv (α : Type u) where
-    inv : α → α
-
-postfix:max "⁻¹" => Inv.inv
-
 export Zero (zero)
 
 instance [Zero α] : OfNat α (nat_lit 0) where

tests/lean/run/alg.lean

@@ -29,11 +29,6 @@ instance [CommMonoid α] : CommSemigroup α where
 instance [CommMonoid α] : MulComm α where
   mul_comm := CommSemigroup.mul_comm
 
-class Inv (α : Type u) where
-  inv : α → α
-
-postfix:max "⁻¹" => Inv.inv
-
 class Group (α : Type u) extends Monoid α, Inv α where
   mul_left_inv (a : α) : a⁻¹ * a = 1
 

tests/lean/run/grind_regression.lean

@@ -640,9 +640,6 @@ end
 
 section
 
-class Inv (α) where inv : α → α
-postfix:max "⁻¹" => Inv.inv
-
 class Group (α) extends Mul α, One α, Inv α where
   mul_assoc    (a b c : α) : (a * b) * c = a * (b * c)
   one_mul      (a : α)     : 1 * a = a

tests/lean/run/mathlibetaissue.lean

@@ -44,7 +44,6 @@ end Std.Classes.RatCast
 
 section Mathlib.Algebra.Group.Defs
 
-class Inv (α : Type u) where
 class Semigroup (G : Type u) extends Mul G where
 class AddSemigroup (G : Type u) extends Add G where
 class CommSemigroup (G : Type u) extends Semigroup G where

tests/lean/run/structWithAlgTCSynth.lean

@@ -112,11 +112,6 @@ infixr:73 " • " => HSMul.hSMul
 instance instHSMul [SMul α β] : HSMul α β β where
   hSMul := SMul.smul
 
-class Inv (α : Type u) where
-  inv : α → α
-
-postfix:max "⁻¹" => Inv.inv
-
 class Semigroup (G : Type u) extends Mul G where
   mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)