From 9ef1b528e305c43a77f295f82971f21885a14663 Mon Sep 17 00:00:00 2001 From: Anne Baanen Date: Wed, 11 Feb 2026 14:29:35 +0100 Subject: [PATCH 1/3] chore: link to mathlib4 docs page in library overview This PR fixes a few dead links on the library overview page: we link to docgen pages for modules, rather than a specific declaration there. But those links still used the mathlib3 naming conventions; update to mathlib4. --- docs/overview.yaml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/overview.yaml b/docs/overview.yaml index 771307bcabe793..da0b56d04de969 100644 --- a/docs/overview.yaml +++ b/docs/overview.yaml @@ -244,7 +244,7 @@ Topology: order topology: 'OrderTopology' intermediate value theorem: 'intermediate_value_Icc' extreme value theorem: 'IsCompact.exists_isMinOn' - limit infimum and supremum: 'order/liminf_limsup.html' + limit infimum and supremum: 'mathlib4_docs/Mathlib/Order/LiminfLimsup.html' topological group: 'IsTopologicalGroup' completion of an abelian topological group: 'UniformSpace.Completion.instAddCommGroup' infinite sum: 'HasSum' @@ -306,7 +306,7 @@ Analysis: derivative of the inverse of a function: 'HasFDerivAt.of_local_left_inverse' Rolle's theorem: 'exists_deriv_eq_zero' mean value theorem: 'exists_ratio_deriv_eq_ratio_slope' - Taylor's theorem: 'analysis/calculus/taylor.html' + Taylor's theorem: 'mathlib4_docs/Mathlib/Analysis/Calculus/Taylor.html' $C^k$ function: 'ContDiff' Leibniz formula: 'fderiv_mul' local extrema: 'IsLocalMin.fderiv_eq_zero' @@ -319,7 +319,7 @@ Analysis: characterization of convexity: 'convexOn_of_deriv2_nonneg' Jensen's inequality (finite sum version): 'ConvexOn.map_sum_le' Jensen's inequality (integral version): 'ConvexOn.map_integral_le' - convexity inequalities: 'analysis/mean_inequalities.html' + convexity inequalities: 'mathlib4_docs/Mathlib/Analysis/MeanInequalities.html' Carathéodory's theorem: 'convexHull_eq_union' Special functions: From 05a9b621debead390682cbab2fc8d7f27b72fde5 Mon Sep 17 00:00:00 2001 From: Anne Baanen Date: Wed, 11 Feb 2026 14:31:02 +0100 Subject: [PATCH 2/3] Don't include the docs folder (it is inserted automatically) --- docs/overview.yaml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/overview.yaml b/docs/overview.yaml index da0b56d04de969..eb74a4f96c3769 100644 --- a/docs/overview.yaml +++ b/docs/overview.yaml @@ -244,7 +244,7 @@ Topology: order topology: 'OrderTopology' intermediate value theorem: 'intermediate_value_Icc' extreme value theorem: 'IsCompact.exists_isMinOn' - limit infimum and supremum: 'mathlib4_docs/Mathlib/Order/LiminfLimsup.html' + limit infimum and supremum: 'Mathlib/Order/LiminfLimsup.html' topological group: 'IsTopologicalGroup' completion of an abelian topological group: 'UniformSpace.Completion.instAddCommGroup' infinite sum: 'HasSum' @@ -306,7 +306,7 @@ Analysis: derivative of the inverse of a function: 'HasFDerivAt.of_local_left_inverse' Rolle's theorem: 'exists_deriv_eq_zero' mean value theorem: 'exists_ratio_deriv_eq_ratio_slope' - Taylor's theorem: 'mathlib4_docs/Mathlib/Analysis/Calculus/Taylor.html' + Taylor's theorem: 'Mathlib/Analysis/Calculus/Taylor.html' $C^k$ function: 'ContDiff' Leibniz formula: 'fderiv_mul' local extrema: 'IsLocalMin.fderiv_eq_zero' @@ -319,7 +319,7 @@ Analysis: characterization of convexity: 'convexOn_of_deriv2_nonneg' Jensen's inequality (finite sum version): 'ConvexOn.map_sum_le' Jensen's inequality (integral version): 'ConvexOn.map_integral_le' - convexity inequalities: 'mathlib4_docs/Mathlib/Analysis/MeanInequalities.html' + convexity inequalities: 'Mathlib/Analysis/MeanInequalities.html' Carathéodory's theorem: 'convexHull_eq_union' Special functions: From 2f1468803c45599c3f8779757177246ffd3fef6d Mon Sep 17 00:00:00 2001 From: "Anne C.A. Baanen" Date: Fri, 13 Feb 2026 14:12:18 +0100 Subject: [PATCH 3/3] Update `undergrad.yaml` too --- docs/undergrad.yaml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/undergrad.yaml b/docs/undergrad.yaml index d826cac30a1997..6295168a54236f 100644 --- a/docs/undergrad.yaml +++ b/docs/undergrad.yaml @@ -172,7 +172,7 @@ Ring Theory: characteristic of a ring: 'ringChar' characteristic zero: 'CharZero' characteristic p: 'CharP' - Subfields: 'field_theory/subfield.html' + Subfields: 'Subfield' Frobenius morphisms: 'frobenius' field $\Q$ of rational numbers: 'Rat.instField' field $\R$ of real numbers: 'Real.instField' @@ -185,7 +185,7 @@ Ring Theory: algebraically closed fields: 'IsAlgClosed' rupture fields: 'AdjoinRoot' splitting fields: 'Polynomial.SplittingField' - finite fields: 'field_theory/finite.html' + finite fields: 'Mathlib/FieldTheory/Finite/Basic.html' rational fraction fields with one indeterminate over a field: 'RatFunc' $\R(X)$-partial fraction decomposition: 'https://en.wikipedia.org/wiki/Partial_fraction_decomposition#General_result' $\C(X)$-partial fraction decomposition: 'https://en.wikipedia.org/wiki/Partial_fraction_decomposition#Statement' @@ -283,7 +283,7 @@ Single Variable Real Analysis: convergence: 'Filter.Tendsto' limit point: 'MapClusterPt' recurrent sequences: 'Nat' - limit infimum and supremum: 'order/liminf_limsup.html' + limit infimum and supremum: 'Mathlib/Order/LiminfLimsup.html' Cauchy sequences: 'CauchySeq' Topology of R: metric structure: 'Real.metricSpace' @@ -360,7 +360,7 @@ Single Variable Real Analysis: continuity: 'ConvexOn.continuousOn' differentiability: 'https://en.wikipedia.org/wiki/Convex_function#Functions_of_one_variable' characterizations of convexity: 'convexOn_of_deriv2_nonneg' - convexity inequalities: 'analysis/mean_inequalities.html' + convexity inequalities: 'Mathlib/Analysis/MeanInequalities.html' # 7. Single Variable Complex Analysis: