[Merged by Bors] - doc: add wikidata cross references by jcommelin · Pull Request #39909 · leanprover-community/mathlib4

jcommelin · 2026-05-27T08:22:00Z

github-actions · 2026-05-27T08:23:23Z

PR summary 49c90097e6

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Baire.Lemmas	619	620	+1 (+0.16%)

Import changes for all files

Files	Import difference
6 files `Mathlib.Topology.AlexandrovDiscrete` `Mathlib.Topology.Baire.Lemmas` `Mathlib.Topology.Compactness.NhdsKer` `Mathlib.Topology.Inseparable` `Mathlib.Topology.Maps.OpenQuotient` `Mathlib.Topology.NhdsKer`	1

Declarations diff

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

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.

No changes to weak technical debt.

kim-em · 2026-05-27T18:21:39Z

Manual test run of #39876 / #39877 — no action needed. This is what the bot will post automatically on PRs like yours once #39876 (dump script), #39877 (CI workflow), and mathlib-ci#44 (orchestrator) all land. Posted here because your PR is the first real exerciser of the wikidata code path. Generated by running scripts/dump_crossref_tags.lean on a local merge of #39877 + #39909, then feeding the TSV through crossref-render in external-tags with --baseline-tsv (to subtract pre-existing stacks/kerodon tags) and --changed-files (your 13 paths).

(Edited to pick up an external-tags fix: declaration names were being rendered with stray \_ escapes because the renderer was applying full Markdown escaping to text already inside a ` code span.)

Cross-reference review

This PR touches 14 cross-reference tags:

Wikidata

Tag	Title	Description	Declaration
`Q193878`	Chinese remainder theorem	theorem for solving simultaneous congruences	`Ideal.quotientInfRingEquivPiQuotient`
`Q505798`	Lagrange's theorem	group theory	`Subgroup.card_subgroup_dvd_card`
`Q505798`	Lagrange's theorem	group theory	`AddSubgroup.card_addSubgroup_dvd_card`
`Q1052678`	Baire category theorem	theorem in topology and functional analysis	`dense_iInter_of_isOpen`
`Q245098`	intermediate value theorem	theorem	`intermediate_value_Icc`
`Q253214`	Heine–Borel theorem	theorem about compact sets in Euclidean space	`Metric.isCompact_iff_isClosed_bounded`
`Q190546`	Cauchy–Schwarz inequality	a useful inequality encountered in many different settings, such as linear algebra, analysis, probability theory, vector algebra and other areas. It is considered to be one of the most important inequalities in all of mathematics	`inner_mul_inner_self_le`
`Q193286`	Rolle's theorem	on stationary points between two equal values of a real differentiable function	`exists_deriv_eq_zero`
`Q189136`	mean value theorem	on the existence of a tangent to an arc parallel to the line through its endpoints	`exists_ratio_deriv_eq_ratio_slope`
`Q866116`	Hahn–Banach theorem	theorem on extension of bounded linear functionals	`exists_extension_norm_eq`
`Q192760`	fundamental theorem of algebra	Every polynomial has a real or complex root	`Complex.isAlgClosed`
`Q939927`	Stone–Weierstrass theorem	theorem that every continuous function on a compact Hausdorff space can be approximated by certain families of continuous functions	`ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints`
`Q1816967`	Urysohn's lemma	lemma that a topological space is normal iff any 2 disjoint closed subsets can be separated by a continuous function	`exists_continuous_zero_one_of_isClosed`
`Q220680`	Banach fixed-point theorem	theorem about metric spaces	`ContractingWith.exists_fixedPoint`

_{Posted by external-tags. Snippets are fetched from upstream live. This check is advisory: the dump script runs from the PR checkout, so a PR can edit the producer to hide tags from this comment.}

jcommelin · 2026-05-28T13:00:07Z


 /-- Baire theorem: a countable intersection of dense open sets is dense. Formulated here with
 an index set which is a countable type. -/
+@[wikidata Q1052678]


Wikidata Q1052678: Baire category theorem — theorem in topology and functional analysis

jcommelin · 2026-05-28T13:00:07Z

 * `f` equals one on `t`;
 * `0 ≤ f x ≤ 1` for all `x`.
 -/
+@[wikidata Q1816967]


Wikidata Q1816967: Urysohn's lemma — lemma that a topological space is normal iff any 2 disjoint closed subsets can be separated by a continuous function

jcommelin · 2026-05-28T13:00:07Z


 include hab hfc hgc hgd hfd in
 /-- Cauchy's Mean Value Theorem, `deriv` version. -/
+@[wikidata Q189136]


Wikidata Q189136: mean value theorem — on the existence of a tangent to an arc parallel to the line through its endpoints

jcommelin · 2026-05-28T13:00:08Z

  ring

 /-- **Cauchy–Schwarz inequality**. -/
+@[wikidata Q190546]


Wikidata Q190546: Cauchy–Schwarz inequality — a useful inequality encountered in many different settings, such as linear algebra, analysis, probability theory, vector algebra and other areas. It is considered to be one of the most important inequalities in all of mathematics

Can we have multiple instances of a single tag? If so I'd advocate also linking to this from LinearMap.BilinForm.apply_mul_apply_le_of_forall_zero_le.

jcommelin · 2026-05-28T13:00:08Z

  simp at hf

+/-- **Fundamental theorem of algebra**: the field `ℂ` of complex numbers is algebraically closed. -/
+@[wikidata Q192760]


Wikidata Q192760: fundamental theorem of algebra — Every polynomial has a real or complex root

jcommelin · 2026-05-28T13:00:08Z


 /-- **Intermediate Value Theorem** for continuous functions on closed intervals, case
 `f a ≤ t ≤ f b`. -/
+@[wikidata Q245098]


Wikidata Q245098: intermediate value theorem — theorem

jcommelin · 2026-05-28T13:00:08Z

 -- TODO: assume `[MetricSpace α]` instead of `[PseudoMetricSpace α] [T2Space α]`
 /-- The **Heine–Borel theorem**:
 In a proper Hausdorff space, a set is compact if and only if it is closed and bounded. -/
+@[wikidata Q253214]


Wikidata Q253214: Heine–Borel theorem — theorem about compact sets in Euclidean space

jcommelin · 2026-05-28T13:00:08Z

 /-- **Lagrange's Theorem**: The order of a subgroup divides the order of its ambient group. -/
-@[to_additive /-- **Lagrange's Theorem**: The order of an additive subgroup divides the order of its
-ambient additive group. -/]
+@[to_additive (attr := wikidata Q505798) /-- **Lagrange's Theorem**: The order of an additive


Wikidata Q505798: Lagrange's theorem — group theory

jcommelin · 2026-05-28T13:00:08Z


 /-- **Hahn-Banach theorem** for continuous linear functions over `𝕜`
 satisfying `IsRCLikeNormedField 𝕜`. -/
+@[wikidata Q866116]


Wikidata Q866116: Hahn–Banach theorem — theorem on extension of bounded linear functionals

jcommelin · 2026-05-28T13:00:08Z

 that a subalgebra `A` of `C(X, ℝ)`, where `X` is a compact topological space,
 is dense if it separates points.
 -/
+@[wikidata Q939927]


Wikidata Q939927: Stone–Weierstrass theorem — theorem that every continuous function on a compact Hausdorff space can be approximated by certain families of continuous functions

ocfnash

One suggestion. Otherwise LGTM.

bors d+

ocfnash · 2026-05-28T13:37:18Z

  ring

 /-- **Cauchy–Schwarz inequality**. -/
+@[wikidata Q190546]


Can we have multiple instances of a single tag? If so I'd advocate also linking to this from LinearMap.BilinForm.apply_mul_apply_le_of_forall_zero_le.

mathlib-bors · 2026-05-28T13:39:40Z

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

mathlib-auto-merge · 2026-05-29T06:27:19Z

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

mathlib-bors · 2026-05-29T07:06:29Z

Pull request successfully merged into master.

Build succeeded:

doc: add wikidata cross references

e26f106

add crossref attribute import

2956e80

kim-em mentioned this pull request May 27, 2026

feat(scripts): dump cross-reference tags to TSV for downstream review #39876

Open

kim-em mentioned this pull request May 27, 2026

fix(render): don't markdown-escape values rendered inside code spans leanprover-community/external-tags#1

Merged

jcommelin marked this pull request as ready for review May 28, 2026 06:22

jcommelin commented May 28, 2026

View reviewed changes

ocfnash approved these changes May 28, 2026

View reviewed changes

mathlib-triage Bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label May 28, 2026

more Cauchy-Schwarz

49c9009

jcommelin added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label May 29, 2026

mathlib-bors Bot pushed a commit that referenced this pull request May 29, 2026

doc: add wikidata cross references (#39909)

10053ce

mathlib-bors Bot changed the title ~~doc: add wikidata cross references~~ [Merged by Bors] - doc: add wikidata cross references May 29, 2026

mathlib-bors Bot closed this May 29, 2026

grunweg pushed a commit to grunweg/mathlib4 that referenced this pull request May 30, 2026

doc: add wikidata cross references (leanprover-community#39909)

32ac986

b-mehta pushed a commit to b-mehta/mathlib4 that referenced this pull request Jun 2, 2026

doc: add wikidata cross references (leanprover-community#39909)

8199322

Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026

doc: add wikidata cross references (leanprover-community#39909)

061cc39

Uh oh!

Conversation

jcommelin commented May 27, 2026

Uh oh!

github-actions Bot commented May 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 49c90097e6

Import changes for modified files

Declarations diff

Uh oh!

kim-em commented May 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Cross-reference review

Wikidata

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ocfnash left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mathlib-bors Bot commented May 28, 2026

Uh oh!

mathlib-auto-merge Bot commented May 29, 2026

Uh oh!

mathlib-bors Bot commented May 29, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

github-actions Bot commented May 27, 2026 •

edited

Loading

kim-em commented May 27, 2026 •

edited

Loading