chore: change pp_nodot adaptation note links to lean4 issue #1910 t…

…o refer to lean4 issue #6178 instead  (#19385)

These adaptation notes refer to the `pp_nodot` attribute not doing anything on certain declarations, due to their inability to be used with dot notation. However, now that leanprover/lean4#1910 has been fixed, the limiting factor has become the fact that the pretty printer doesn't work for these kinds of dot notation, which leanprover/lean4#6178 is an issue for.

As such, the links to the blocking lean issue have been changed in this PR.

Mathlib/Algebra/Symmetrized.lean

@@ -48,7 +48,7 @@ def sym : α ≃ αˢʸᵐ :=
 
 /-- The element of `α` represented by `x : αˢʸᵐ`. -/
 -- Porting note (kmill): `pp_nodot` has no affect here
--- unless RFC https://github.com/leanprover/lean4/issues/1910 leads to dot notation for CoeFun
+-- unless RFC https://github.com/leanprover/lean4/issues/6178 leads to dot notation pp for CoeFun
 @[pp_nodot]
 def unsym : αˢʸᵐ ≃ α :=
   Equiv.refl _

Mathlib/Data/NNReal/Defs.lean

@@ -917,7 +917,7 @@ namespace Real
 
 /-- The absolute value on `ℝ` as a map to `ℝ≥0`. -/
 -- Porting note (kmill): `pp_nodot` has no affect here
--- unless RFC https://github.com/leanprover/lean4/issues/1910 leads to dot notation for CoeFun
+-- unless RFC https://github.com/leanprover/lean4/issues/6178 leads to dot notation pp for CoeFun
 @[pp_nodot]
 def nnabs : ℝ →*₀ ℝ≥0 where
   toFun x := ⟨|x|, abs_nonneg x⟩

Mathlib/Data/Real/Sqrt.lean

@@ -39,7 +39,7 @@ variable {x y : ℝ≥0}
 
 /-- Square root of a nonnegative real number. -/
 -- Porting note (kmill): `pp_nodot` has no affect here
--- unless RFC https://github.com/leanprover/lean4/issues/1910 leads to dot notation for CoeFun
+-- unless RFC https://github.com/leanprover/lean4/issues/6178 leads to dot notation pp for CoeFun
 @[pp_nodot]
 noncomputable def sqrt : ℝ≥0 ≃o ℝ≥0 :=
   OrderIso.symm <| powOrderIso 2 two_ne_zero