doc: document some notation (#11922)

We cannot literally use @[inherit_doc] in these cases, but we can slightly modify the underlying docstring or a turn a regular comment into a doc comment.

Mathlib/Algebra/Order/Kleene.lean

@@ -63,6 +63,7 @@ class IdemSemiring (α : Type u) extends Semiring α, SemilatticeSup α where
   protected add_eq_sup : ∀ a b : α, a + b = a ⊔ b := by
     intros
     rfl
+  /-- The bottom element of an idempotent semiring: `0` by default -/
   protected bot : α := 0
   protected bot_le : ∀ a, bot ≤ a
 #align idem_semiring IdemSemiring
@@ -74,11 +75,12 @@ class IdemCommSemiring (α : Type u) extends CommSemiring α, IdemSemiring α
 
 /-- Notation typeclass for the Kleene star `∗`. -/
 class KStar (α : Type*) where
+  /-- The Kleene star operator on a Kleene algebra -/
   protected kstar : α → α
 #align has_kstar KStar
 
--- mathport name: «expr ∗»
-scoped[Computability] postfix:1024 "∗" => KStar.kstar
+@[inherit_doc] scoped[Computability] postfix:1024 "∗" => KStar.kstar
+
 open Computability
 
 /-- A Kleene Algebra is an idempotent semiring with an additional unary operator `kstar` (for Kleene

Mathlib/AlgebraicTopology/SimplicialSet.lean

@@ -78,7 +78,6 @@ def standardSimplex : SimplexCategory ⥤ SSet.{u} :=
 set_option linter.uppercaseLean3 false in
 #align sSet.standard_simplex SSet.standardSimplex
 
--- mathport name: standard_simplex
 @[inherit_doc SSet.standardSimplex]
 scoped[Simplicial] notation3 "Δ[" n "]" => SSet.standardSimplex.obj (SimplexCategory.mk n)
 
@@ -173,7 +172,7 @@ def boundary (n : ℕ) : SSet.{u} where
 set_option linter.uppercaseLean3 false in
 #align sSet.boundary SSet.boundary
 
--- mathport name: sSet.boundary
+/-- The boundary `∂Δ[n]` of the `n`-th standard simplex -/
 scoped[Simplicial] notation3 "∂Δ[" n "]" => SSet.boundary n
 
 /-- The inclusion of the boundary of the `n`-th standard simplex into that standard simplex. -/
@@ -197,7 +196,7 @@ def horn (n : ℕ) (i : Fin (n + 1)) : SSet where
 set_option linter.uppercaseLean3 false in
 #align sSet.horn SSet.horn
 
--- mathport name: sSet.horn
+/-- The `i`-th horn `Λ[n, i]` of the standard `n`-simplex -/
 scoped[Simplicial] notation3 "Λ[" n ", " i "]" => SSet.horn (n : ℕ) i
 
 /-- The inclusion of the `i`-th horn of the `n`-th standard simplex into that standard simplex. -/

Mathlib/Data/Set/Sups.lean

@@ -37,20 +37,22 @@ variable {F α β : Type*}
 
 /-- Notation typeclass for pointwise supremum `⊻`. -/
 class HasSups (α : Type*) where
+  /-- The point-wise supremum `a ⊔ b` of `a, b : α`. -/
   sups : α → α → α
 #align has_sups HasSups
 
 /-- Notation typeclass for pointwise infimum `⊼`. -/
 class HasInfs (α : Type*) where
+  /-- The point-wise infimum `a ⊓ b` of `a, b : α`. -/
   infs : α → α → α
 #align has_infs HasInfs
 
--- mathport name: «expr ⊻ »
+-- This notation is meant to have higher precedence than `⊔` and `⊓`, but still within the
+-- realm of other binary notation.
+@[inherit_doc]
 infixl:74 " ⊻ " => HasSups.sups
-  -- This notation is meant to have higher precedence than `⊔` and `⊓`, but still within the
-  -- realm of other binary notation
 
--- mathport name: «expr ⊼ »
+@[inherit_doc]
 infixl:75 " ⊼ " => HasInfs.infs
 
 namespace Set

Mathlib/Data/Tree.lean

@@ -145,7 +145,7 @@ def right : Tree α → Tree α
   | node _ _l r => r
 #align tree.right Tree.right
 
--- Notation for making a node with `Unit` data
+/-- A node with `Unit` data -/
 scoped infixr:65 " △ " => Tree.node ()
 
 -- Porting note: workaround for leanprover/lean4#2049

Mathlib/Init/Algebra/Classes.lean

@@ -416,8 +416,8 @@ instance isEquiv : IsEquiv α (@Equiv _ r) where
 
 end
 
-notation:50 -- Notation for the equivalence relation induced by lt
-a " ≈[" lt "]" b:50 => @Equiv _ lt a b
+/-- The equivalence relation induced by `lt` -/
+notation:50 a " ≈[" lt "]" b:50 => @Equiv _ lt a b--Equiv (r := lt) a b
 
 end StrictWeakOrder
 

Mathlib/Topology/Homotopy/HSpaces.lean

@@ -71,7 +71,7 @@ class HSpace (X : Type u) [TopologicalSpace X] where
     (hmul.comp <| (ContinuousMap.id X).prodMk <| const X e).HomotopyRel (ContinuousMap.id X) {e}
 #align H_space HSpace
 
--- We use the notation `⋀`, typeset as \And, to denote the binary operation `hmul` on an H-space
+/-- The binary operation `hmul` on an `H`-space -/
 scoped[HSpaces] notation x "⋀" y => HSpace.hmul (x, y)
 
 -- Porting note: opening `HSpaces` so that the above notation works

scripts/nolints.json

@@ -63,8 +63,6 @@
  ["docBlame", "«term_≃ᵃⁱ[_]_»"],
  ["docBlame", "«term_≃ᵈ_»"],
  ["docBlame", "«term_≡_[SMOD_]»"],
- ["docBlame", "«term_⊻_»"],
- ["docBlame", "«term_⊼_»"],
  ["docBlame", "termℤ"],
  ["docBlame", "«termℤ√_»"],
  ["docBlame", "«term∃!_,_»"],
@@ -123,7 +121,6 @@
  ["docBlame", "Complex.«term_×ℂ_»"],
  ["docBlame", "CompositionSeries.length"],
  ["docBlame", "CompositionSeries.series"],
- ["docBlame", "Computability.«term_∗»"],
  ["docBlame", "Computation.parallelRec"],
  ["docBlame", "Congr!.elabConfig"],
  ["docBlame", "ContDiffBump.rIn"],
@@ -205,10 +202,7 @@
  ["docBlame", "HSpace.eHmul"],
  ["docBlame", "HSpace.hmul"],
  ["docBlame", "HSpace.hmulE"],
- ["docBlame", "HSpaces.«term_⋀_»"],
  ["docBlame", "HahnSeries.coeff"],
- ["docBlame", "HasInfs.infs"],
- ["docBlame", "HasSups.sups"],
  ["docBlame", "Holor.assocLeft"],
  ["docBlame", "Holor.assocRight"],
  ["docBlame", "HolorIndex.assocLeft"],
@@ -223,8 +217,6 @@
  ["docBlame", "HomotopyEquiv.homotopyInvHomId"],
  ["docBlame", "HomotopyEquiv.inv"],
  ["docBlame", "IO.runRandWith"],
- ["docBlame", "IdemCommSemiring.bot"],
- ["docBlame", "IdemSemiring.bot"],
  ["docBlame", "ImplicitFunctionData.leftDeriv"],
  ["docBlame", "ImplicitFunctionData.leftFun"],
  ["docBlame", "ImplicitFunctionData.pt"],
@@ -243,7 +235,6 @@
  ["docBlame", "Isocrystal.«termφ(_,_)»"],
  ["docBlame", "JordanHolderLattice.IsMaximal"],
  ["docBlame", "JordanHolderLattice.Iso"],
- ["docBlame", "KStar.kstar"],
  ["docBlame", "Kronecker.«term_⊗ₖ_»"],
  ["docBlame", "Kronecker.«term_⊗ₖₜ[_]_»"],
  ["docBlame", "Kronecker.«term_⊗ₖₜ_»"],
@@ -403,8 +394,6 @@
  ["docBlame", "SemigroupCat.forget_obj_eq_coe"],
  ["docBlame", "Set.«term{_|_}»"],
  ["docBlame", "Shrink.rec"],
- ["docBlame", "Simplicial.«termΛ[_,_]»"],
- ["docBlame", "Simplicial.«term∂Δ[_]»"],
  ["docBlame", "SlashAction.map"],
  ["docBlame", "SlashInvariantForm.toFun"],
  ["docBlame", "SlimCheck.NamedBinder"],
@@ -424,7 +413,6 @@
  ["docBlame", "Stream'.«term_⋈_»"],
  ["docBlame", "Stream'.unfolds"],
  ["docBlame", "StrictWeakOrder.Equiv"],
- ["docBlame", "StrictWeakOrder.«term_≈[_]_»"],
  ["docBlame", "StructureGroupoid.members"],
  ["docBlame", "Submodule.«term_∙_»"],
  ["docBlame", "Topology.«termI^_»"],
@@ -436,7 +424,6 @@
  ["docBlame", "Traversable.foldrm"],
  ["docBlame", "Traversable.length"],
  ["docBlame", "Traversable.mapFold"],
- ["docBlame", "Tree.«term_△_»"],
  ["docBlame", "Tree.unitRecOn"],
  ["docBlame", "Trivialization.baseSet"],
  ["docBlame", "UFModel.Agrees"],