add @[inherit_doc] to equiv notation (#7998)

This makes hovering over `≃` display the docstring for `Equiv` (if I've understood things correctly).
leanprover-community · Oct 28, 2023 · 2aead33 · 2aead33
1 parent d70b029
commit 2aead33
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Mathlib/Logic/Equiv/Defs.lean b/Mathlib/Logic/Equiv/Defs.lean
@@ -70,6 +70,7 @@ structure Equiv (α : Sort*) (β : Sort _) where
   protected right_inv : RightInverse invFun toFun
 #align equiv Equiv
 
+@[inherit_doc]
 infixl:25 " ≃ " => Equiv
 
 /-- Turn an element of a type `F` satisfying `EquivLike F α β` into an actual