Skip to content

[Merged by Bors] - chore: link to mathlib4 docs page in library overview #35129

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
Vierkantor wants to merge 3 commits into from
+7 −7
Closed

[Merged by Bors] - chore: link to mathlib4 docs page in library overview #35129

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
9ef1b52
chore: link to mathlib4 docs page in library overview
Vierkantor Feb 11, 2026
05a9b62
Don't include the docs folder (it is inserted automatically)
Vierkantor Feb 11, 2026
2f14688
Update `undergrad.yaml` too
Vierkantor Feb 13, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions docs/overview.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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: 'Mathlib/Order/LiminfLimsup.html'
topological group: 'IsTopologicalGroup'
completion of an abelian topological group: 'UniformSpace.Completion.instAddCommGroup'
infinite sum: 'HasSum'
Expand Down Expand Up @@ -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: 'Mathlib/Analysis/Calculus/Taylor.html'
$C^k$ function: 'ContDiff'
Leibniz formula: 'fderiv_mul'
local extrema: 'IsLocalMin.fderiv_eq_zero'
Expand All @@ -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: 'Mathlib/Analysis/MeanInequalities.html'
Carathéodory's theorem: 'convexHull_eq_union'

Special functions:
Expand Down
8 changes: 4 additions & 4 deletions docs/undergrad.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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'
Expand All @@ -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'
Expand Down Expand Up @@ -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'
Expand Down Expand Up @@ -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:
Expand Down
Loading