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

[Vierkantor]

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.

---

[github-actions]

PR summary 0528bce2a0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Komyyy]

Thank you for your contribution!

Currently, on the overview page, "limit infimum and supremum" links to https://leanprover-community.github.io/mathlib4_docs/order/liminf_limsup.html, which returns 404 error.
So this change is reasonable.

Indeed, the linking is done in the following two piexes of code:

https://github.com/leanprover-community/leanprover-community.github.io/blob/57f641fef6c46443e96fc4519e6755d129dca8e2/make_site.py#L477-L493

https://github.com/leanprover-community/leanprover-community.github.io/blob/57f641fef6c46443e96fc4519e6755d129dca8e2/make_site.py#L428-L438

According to this code, your change will probably work fine.

However, could you also update the following links in undergrad.yaml?

mathlib4/docs/undergrad.yaml

Line 175 in 05a9b62

Subfields: 'field_theory/subfield.html'

mathlib4/docs/undergrad.yaml

Line 188 in 05a9b62

finite fields: 'field_theory/finite.html'

mathlib4/docs/undergrad.yaml

Line 286 in 05a9b62

limit infimum and supremum: 'order/liminf_limsup.html'

mathlib4/docs/undergrad.yaml

Line 363 in 05a9b62

convexity inequalities: 'analysis/mean_inequalities.html'

[bryangingechen]

Thanks to @Komyyy for linking to the places where the links are written! That saved me quite a bit of time.

And thanks also for pointing out the undergrad.yaml links as well. However, I think that could either be done in this PR or another one; either way is fine. I'll leave it to @Vierkantor.

Thanks!
bors d+

[mathlib-bors]

✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[Vierkantor]

I've updated subfields to refer to Subfield, since the contents of Subfield.lean ended up being split over a Defs file, a Basic file and some more. Or is there a particular set of results about subfields we want to refer to here?

[Komyyy]

Thank you!

Speaking from my experience, people new to Lean or Mathlib will first want to look up definitions, so I think keeping it as Subfield is fine.

[Vierkantor]

The reason I ask is that undergrad.yaml is a reference to a specific document (the undergraduate maths curriculum in France), so they might have in mind a precise set of results we want to have on subfields. But looking at the original PR that added the link, I can't see anything more specific. So I'm going to assume it is fine to merge this PR.

bors r+

[mathlib-bors]

Build failed:

• ci (staging) / Post-CI job

[Vierkantor]

Not sure what happened here, it just says the post-build job was skipped? I'm going to retry.

bors r+

[mathlib-bors]

Build failed:

• ci (staging) / Post-Build Step

[bryangingechen]

Ah, this ran into the issue that #35389 fixed. Let's try again.

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Lint style
• ci (staging) / Build
• ci (staging) / Post-CI job
• ci (staging) / Post-Build Step