chore: classify removed @[pp_nodot] porting notes (#11181)

Classifies by adding issue number #11180 to porting notes claiming: > removed `@[pp_nodot]`
leanprover-community · Mar 12, 2024 · c30fa3d · c30fa3d
1 parent b55aaee
commit c30fa3d
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/Mathlib/Algebra/Symmetrized.lean b/Mathlib/Algebra/Symmetrized.lean
@@ -47,13 +47,13 @@ variable {α : Type*}
 
 /-- The element of `SymAlg α` that represents `a : α`. -/
 @[match_pattern]
--- Porting note: removed @[pp_nodot]
+-- Porting note (#11180): removed @[pp_nodot]
 def sym : α ≃ αˢʸᵐ :=
   Equiv.refl _
 #align sym_alg.sym SymAlg.sym
 
 /-- The element of `α` represented by `x : αˢʸᵐ`. -/
--- Porting note: removed @[pp_nodot]
+-- Porting note (#11180): removed @[pp_nodot]
 def unsym : αˢʸᵐ ≃ α :=
   Equiv.refl _
 #align sym_alg.unsym SymAlg.unsym

diff --git a/Mathlib/Data/Nat/Prime.lean b/Mathlib/Data/Nat/Prime.lean
@@ -43,7 +43,7 @@ variable {n : ℕ}
 
 /-- `Nat.Prime p` means that `p` is a prime number, that is, a natural number
   at least 2 whose only divisors are `p` and `1`. -/
--- Porting note: removed @[pp_nodot]
+-- Porting note (#11180): removed @[pp_nodot]
 def Prime (p : ℕ) :=
   Irreducible p
 #align nat.prime Nat.Prime

diff --git a/Mathlib/Data/Real/NNReal.lean b/Mathlib/Data/Real/NNReal.lean
@@ -1155,7 +1155,7 @@ end Set
 namespace Real
 
 /-- The absolute value on `ℝ` as a map to `ℝ≥0`. -/
--- Porting note: removed @[pp_nodot]
+-- Porting note (#11180): removed @[pp_nodot]
 def nnabs : ℝ →*₀ ℝ≥0 where
   toFun x := ⟨|x|, abs_nonneg x⟩
   map_zero' := by ext; simp