docs: replace ⬝ BLACK VERY SMALL SQUARE with · MIDDLE DOT (#6522)

`MIDDLE DOT` is now valid Lean syntax for function arguments, which is what these docstrings are referring to.
leanprover-community · Aug 11, 2023 · 30b7080 · 30b7080
1 parent cf85b04
commit 30b7080
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/Mathlib/Analysis/Normed/Group/Basic.lean b/Mathlib/Analysis/Normed/Group/Basic.lean
@@ -494,14 +494,14 @@ open Lean Meta Qq Function
 `norm_nonneg'`. -/
 @[positivity Norm.norm _]
 def evalMulNorm : PositivityExt where eval {_ _} _zα _pα e := do
-  let .app _ a ← whnfR e | throwError "not ‖ ⬝ ‖"
+  let .app _ a ← whnfR e | throwError "not ‖ · ‖"
   let p ← mkAppM ``norm_nonneg' #[a]
   pure (.nonnegative p)
 
 /-- Extension for the `positivity` tactic: additive norms are nonnegative, via `norm_nonneg`. -/
 @[positivity Norm.norm _]
 def evalAddNorm : PositivityExt where eval {_ _} _zα _pα e := do
-  let .app _ a ← whnfR e | throwError "not ‖ ⬝ ‖"
+  let .app _ a ← whnfR e | throwError "not ‖ · ‖"
   let p ← mkAppM ``norm_nonneg #[a]
   pure (.nonnegative p)
 

diff --git a/Mathlib/Analysis/NormedSpace/BanachSteinhaus.lean b/Mathlib/Analysis/NormedSpace/BanachSteinhaus.lean
@@ -75,7 +75,7 @@ open ENNReal
 
 open ENNReal
 
-/-- This version of Banach-Steinhaus is stated in terms of suprema of `↑‖⬝‖₊ : ℝ≥0∞`
+/-- This version of Banach-Steinhaus is stated in terms of suprema of `↑‖·‖₊ : ℝ≥0∞`
 for convenience. -/
 theorem banach_steinhaus_iSup_nnnorm {ι : Type*} [CompleteSpace E] {g : ι → E →SL[σ₁₂] F}
     (h : ∀ x, ⨆ i, ↑‖g i x‖₊ < ∞) : ⨆ i, ↑‖g i‖₊ < ∞ := by

diff --git a/Mathlib/Analysis/NormedSpace/Spectrum.lean b/Mathlib/Analysis/NormedSpace/Spectrum.lean
@@ -47,7 +47,7 @@ This file contains the basic theory for the resolvent and spectrum of a Banach a
 
 open scoped ENNReal NNReal
 
-/-- The *spectral radius* is the supremum of the `nnnorm` (`‖⬝‖₊`) of elements in the spectrum,
+/-- The *spectral radius* is the supremum of the `nnnorm` (`‖·‖₊`) of elements in the spectrum,
     coerced into an element of `ℝ≥0∞`. Note that it is possible for `spectrum 𝕜 a = ∅`. In this
     case, `spectralRadius a = 0`. It is also possible that `spectrum 𝕜 a` be unbounded (though
     not for Banach algebras, see `spectrum.is_bounded`, below).  In this case,