doc(*): fix broken markdown links (#12385)

Some urls to nLab were also weird, so I replaced it with less weird ones. The `MM91` reference was presumably intended to reference `MM92`.
leanprover-community · Mar 2, 2022 · 9daa233 · 9daa233
1 parent b77ff23
commit 9daa233
Show file tree

Hide file tree

Showing 11 changed files with 17 additions and 17 deletions.
diff --git a/src/algebra/group/freiman.lean b/src/algebra/group/freiman.lean
@@ -34,7 +34,7 @@ an `add_monoid`/`monoid` instead of the `add_monoid`/`monoid` itself.
 
 ## References
 
-[Yufei Zhao, *18.225: Graph Theory and Additive Combinatorics][https://yufeizhao.com/gtac/]
+[Yufei Zhao, *18.225: Graph Theory and Additive Combinatorics*](https://yufeizhao.com/gtac/)
 
 ## TODO
 

diff --git a/src/category_theory/category/PartialFun.lean b/src/category_theory/category/PartialFun.lean
@@ -22,8 +22,8 @@ constructive.
 
 ## References
 
-* [nLab, *The category of sets and partial functions]
-[http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/partial+function]
+* [nLab, *The category of sets and partial functions*]
+  (https://ncatlab.org/nlab/show/partial+function)
 -/
 
 open category_theory option

diff --git a/src/category_theory/category/Twop.lean b/src/category_theory/category/Twop.lean
@@ -14,7 +14,7 @@ This defines `Twop`, the category of two-pointed types.
 ## References
 
 * [nLab, *coalgebra of the real interval*]
-[http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/coalgebra+of+the+real+interval]
+  (https://ncatlab.org/nlab/show/coalgebra+of+the+real+interval)
 -/
 
 open category_theory option

diff --git a/src/category_theory/sites/grothendieck.lean b/src/category_theory/sites/grothendieck.lean
@@ -33,12 +33,12 @@ Grothendieck topology, coverage, pretopology, site
 
 ## References
 
-* [https://ncatlab.org/nlab/show/Grothendieck+topology][nlab]
-* [S. MacLane, I. Moerdijk, *Sheaves in Geometry and Logic*][MM91]
+* [nLab, *Grothendieck topology*](https://ncatlab.org/nlab/show/Grothendieck+topology)
+* [S. MacLane, I. Moerdijk, *Sheaves in Geometry and Logic*][MM92]
 
 ## Implementation notes
 
-We use the definition of [nlab] and [MM91](Chapter III, Section 2), where Grothendieck topologies
+We use the definition of [nlab] and [MM92][] (Chapter III, Section 2), where Grothendieck topologies
 are saturated collections of morphisms, rather than the notions of the Stacks project (00VG) and
 the Elephant, in which topologies are allowed to be unsaturated, and are then completed.
 TODO (BM): Add the definition from Stacks, as a pretopology, and complete to a topology.
@@ -65,7 +65,7 @@ three axioms:
 
 A sieve `S` on `X` is referred to as `J`-covering, (or just covering), if `S ∈ J X`.
 
-See https://stacks.math.columbia.edu/tag/00Z4, or [nlab], or [MM92] Chapter III, Section 2,
+See https://stacks.math.columbia.edu/tag/00Z4, or [nlab], or [MM92][] Chapter III, Section 2,
 Definition 1.
 -/
 structure grothendieck_topology :=

diff --git a/src/category_theory/sites/pretopology.lean b/src/category_theory/sites/pretopology.lean
@@ -24,9 +24,9 @@ coverage, pretopology, site
 
 ## References
 
-* [https://ncatlab.org/nlab/show/Grothendieck+pretopology][nlab]
+* [nLab, *Grothendieck pretopology*](https://ncatlab.org/nlab/show/Grothendieck+pretopology)
 * [S. MacLane, I. Moerdijk, *Sheaves in Geometry and Logic*][MM92]
-* [https://stacks.math.columbia.edu/tag/00VG][Stacks]
+* [Stacks, *00VG*](https://stacks.math.columbia.edu/tag/00VG)
 -/
 
 universes v u

diff --git a/src/category_theory/sites/spaces.lean b/src/category_theory/sites/spaces.lean
@@ -23,7 +23,7 @@ site, Grothendieck topology, space
 
 ## References
 
-* [https://ncatlab.org/nlab/show/Grothendieck+topology][nlab]
+* [nLab, *Grothendieck topology*](https://ncatlab.org/nlab/show/Grothendieck+topology)
 * [S. MacLane, I. Moerdijk, *Sheaves in Geometry and Logic*][MM92]
 
 ## Implementation notes

diff --git a/src/data/nat/sqrt.lean b/src/data/nat/sqrt.lean
@@ -16,7 +16,7 @@ representation by replacing the multiplication by 2 appearing in
 ## Reference
 
 See [Wikipedia, *Methods of computing square roots*]
-[https://en.wikipedia.org/wiki/Methods_of_computing_square_roots#Binary_numeral_system_(base_2)].
+(https://en.wikipedia.org/wiki/Methods_of_computing_square_roots#Binary_numeral_system_(base_2)).
 -/
 namespace nat
 

diff --git a/src/data/two_pointing.lean b/src/data/two_pointing.lean
@@ -18,8 +18,8 @@ bipointed types. Two-pointed types form a full subcategory of those.
 
 ## References
 
-[Coalgebra of the real interval]
-[http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/coalgebra+of+the+real+interval]
+* [nLab, *Coalgebra of the real interval*]
+  (https://ncatlab.org/nlab/show/coalgebra+of+the+real+interval)
 -/
 
 open function

diff --git a/src/order/category/DistribLattice.lean b/src/order/category/DistribLattice.lean
@@ -11,7 +11,7 @@ import order.category.Lattice
 This file defines `DistribLattice`, the category of distributive lattices.
 
 Note that `DistribLattice` doesn't correspond to the literature definition of [`DistLat`]
-[https://ncatlab.org/nlab/show/DistLat] as we don't require bottom or top elements. Instead,
+(https://ncatlab.org/nlab/show/DistLat) as we don't require bottom or top elements. Instead,
 `DistLat` corresponds to `BoundedDistribLattice` (not yet in mathlib).
 -/
 

diff --git a/src/order/category/Lattice.lean b/src/order/category/Lattice.lean
@@ -12,7 +12,7 @@ import order.hom.lattice
 This defines `Lattice`, the category of lattices.
 
 Note that `Lattice` doesn't correspond to the literature definition of [`Lat`]
-[https://ncatlab.org/nlab/show/Lat] as we don't require bottom or top elements. Instead, `Lat`
+(https://ncatlab.org/nlab/show/Lat) as we don't require bottom or top elements. Instead, `Lat`
 corresponds to `BoundedLattice` (not yet in mathlib).
 
 ## TODO

diff --git a/src/order/complete_boolean_algebra.lean b/src/order/complete_boolean_algebra.lean
@@ -30,7 +30,7 @@ Add instances for `prod`, `filter`
 
 ## References
 
-* [Wikipedia, *Complete Heyting algebra*][https://en.wikipedia.org/wiki/Complete_Heyting_algebra]
+* [Wikipedia, *Complete Heyting algebra*](https://en.wikipedia.org/wiki/Complete_Heyting_algebra)
 * [Francis Borceux, *Handbook of Categorical Algebra III*][borceux-vol3]
 -/