doc: add wikidata cross references (#39909)

jcommelin · jcommelin · commit 10053cefd9be · 2026-05-29T06:27:39.000Z
diff --git a/Mathlib/Analysis/Calculus/Deriv/MeanValue.lean b/Mathlib/Analysis/Calculus/Deriv/MeanValue.lean
@@ -128,6 +128,7 @@ theorem exists_hasDerivAt_eq_slope : ∃ c ∈ Ioo a b, f' c = (f b - f a) / (b
 
 include hab hfc hgc hgd hfd in
 /-- Cauchy's Mean Value Theorem, `deriv` version. -/
+@[wikidata Q189136]
 theorem exists_ratio_deriv_eq_ratio_slope :
     ∃ c ∈ Ioo a b, (g b - g a) * deriv f c = (f b - f a) * deriv g c :=
   exists_ratio_hasDerivAt_eq_ratio_slope f (deriv f) hab hfc
diff --git a/Mathlib/Analysis/Calculus/LocalExtr/Rolle.lean b/Mathlib/Analysis/Calculus/LocalExtr/Rolle.lean
@@ -55,6 +55,7 @@ theorem exists_hasDerivAt_eq_zero (hab : a < b) (hfc : ContinuousOn f (Icc a b))
   ⟨c, cmem, hc.hasDerivAt_eq_zero <| hff' c cmem⟩
 
 /-- **Rolle's Theorem** `deriv` version -/
+@[wikidata Q193286]
 theorem exists_deriv_eq_zero (hab : a < b) (hfc : ContinuousOn f (Icc a b)) (hfI : f a = f b) :
     ∃ c ∈ Ioo a b, deriv f c = 0 :=
   let ⟨c, cmem, hc⟩ := exists_isLocalExtr_Ioo hab hfc hfI
diff --git a/Mathlib/Analysis/Complex/Polynomial/Basic.lean b/Mathlib/Analysis/Complex/Polynomial/Basic.lean
@@ -47,6 +47,8 @@ theorem exists_root {f : ℂ[X]} (hf : 0 < degree f) : ∃ z : ℂ, IsRoot f z :
   obtain rfl : f = C 0 := Polynomial.funext fun z ↦ inv_injective <| by simp [this]
   simp at hf
 
+/-- **Fundamental theorem of algebra**: the field `ℂ` of complex numbers is algebraically closed. -/
+@[wikidata Q192760]
 instance isAlgClosed : IsAlgClosed ℂ :=
   IsAlgClosed.of_exists_root _ fun _p _ hp => Complex.exists_root <| degree_pos_of_irreducible hp
 
diff --git a/Mathlib/Analysis/InnerProductSpace/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Basic.lean
@@ -278,6 +278,7 @@ theorem parallelogram_law {x y : E} : ⟪x + y, x + y⟫ + ⟪x - y, x - y⟫ =
   ring
 
 /-- **Cauchy–Schwarz inequality**. -/
+@[wikidata Q190546]
 theorem inner_mul_inner_self_le (x y : E) : ‖⟪x, y⟫‖ * ‖⟪y, x⟫‖ ≤ re ⟪x, x⟫ * re ⟪y, y⟫ :=
   letI : PreInnerProductSpace.Core 𝕜 E := PreInnerProductSpace.toCore
   InnerProductSpace.Core.inner_mul_inner_self_le x y
diff --git a/Mathlib/Analysis/Normed/Module/HahnBanach.lean b/Mathlib/Analysis/Normed/Module/HahnBanach.lean
@@ -72,6 +72,7 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜
 
 /-- **Hahn-Banach theorem** for continuous linear functions over `𝕜`
 satisfying `IsRCLikeNormedField 𝕜`. -/
+@[wikidata Q866116]
 theorem exists_extension_norm_eq (p : Subspace 𝕜 E) (f : StrongDual 𝕜 p) :
     ∃ g : StrongDual 𝕜 E, (∀ x : p, g x = f x) ∧ ‖g‖ = ‖f‖ := by
   letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
diff --git a/Mathlib/GroupTheory/Coset/Card.lean b/Mathlib/GroupTheory/Coset/Card.lean
@@ -64,8 +64,8 @@ lemma card_mul_eq_card_subgroup_mul_card_quotient (s : Subgroup α) (t : Set α)
   aesop (add simp [Set.mem_mul])
 
 /-- **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
+subgroup divides the order of its ambient additive group. -/]
 theorem card_subgroup_dvd_card (s : Subgroup α) : Nat.card s ∣ Nat.card α := by
   classical simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_left ℕ]
 
diff --git a/Mathlib/LinearAlgebra/SesquilinearForm/Basic.lean b/Mathlib/LinearAlgebra/SesquilinearForm/Basic.lean
@@ -931,6 +931,7 @@ variable [CommRing R] [LinearOrder R] [IsStrictOrderedRing R]
   [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M)
 
 /-- The **Cauchy-Schwarz inequality** for positive semidefinite forms. -/
+@[wikidata Q190546]
 lemma apply_mul_apply_le_of_forall_zero_le (hs : ∀ x, 0 ≤ B x x) (x y : M) :
     (B x y) * (B y x) ≤ (B x x) * (B y y) := by
   have aux (x y : M) : 0 ≤ (B x x) * ((B x x) * (B y y) - (B x y) * (B y x)) := by
diff --git a/Mathlib/RingTheory/Ideal/Quotient/Operations.lean b/Mathlib/RingTheory/Ideal/Quotient/Operations.lean
@@ -242,6 +242,7 @@ lemma quotientInfToPiQuotient_surj {I : ι → Ideal R}
 
 /-- **Chinese Remainder Theorem**. Eisenbud Ex.2.6.
 Similar to Atiyah-Macdonald 1.10 and Stacks 00DT -/
+@[wikidata Q193878]
 noncomputable def quotientInfRingEquivPiQuotient (f : ι → Ideal R)
     (hf : Pairwise (IsCoprime on f)) : (R ⧸ ⨅ i, f i) ≃+* ∀ i, R ⧸ f i :=
   { Equiv.ofBijective _ ⟨quotientInfToPiQuotient_inj f, quotientInfToPiQuotient_surj hf⟩,
diff --git a/Mathlib/Topology/Baire/Lemmas.lean b/Mathlib/Topology/Baire/Lemmas.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Data.Fintype.Powerset
 public import Mathlib.Topology.GDelta.Basic
 public import Mathlib.Topology.Constructions
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # Baire spaces
@@ -127,6 +128,7 @@ theorem dense_biInter_of_isOpen {S : Set α} {f : α → Set X} (ho : ∀ s ∈
 
 /-- Baire theorem: a countable intersection of dense open sets is dense. Formulated here with
 an index set which is a countable type. -/
+@[wikidata Q1052678]
 theorem dense_iInter_of_isOpen [Countable ι] {f : ι → Set X} (ho : ∀ i, IsOpen (f i))
     (hd : ∀ i, Dense (f i)) : Dense (⋂ s, f s) :=
   dense_sInter_of_isOpen (forall_mem_range.2 ho) (countable_range _) (forall_mem_range.2 hd)
diff --git a/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean b/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
@@ -262,6 +262,7 @@ theorem sublattice_closure_eq_top (L : Set C(X, ℝ)) (nA : L.Nonempty)
 that a subalgebra `A` of `C(X, ℝ)`, where `X` is a compact topological space,
 is dense if it separates points.
 -/
+@[wikidata Q939927]
 theorem subalgebra_topologicalClosure_eq_top_of_separatesPoints (A : Subalgebra ℝ C(X, ℝ))
     (w : A.SeparatesPoints) : A.topologicalClosure = ⊤ := by
   -- The closure of `A` is closed under taking `sup` and `inf`,
diff --git a/Mathlib/Topology/MetricSpace/Bounded.lean b/Mathlib/Topology/MetricSpace/Bounded.lean
@@ -332,6 +332,7 @@ theorem _root_.Bornology.IsBounded.isCompact_closure [ProperSpace α] (h : IsBou
 -- 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]
 theorem isCompact_iff_isClosed_bounded [T2Space α] [ProperSpace α] :
     IsCompact s ↔ IsClosed s ∧ IsBounded s :=
   ⟨fun h => ⟨h.isClosed, h.isBounded⟩, fun h => isCompact_of_isClosed_isBounded h.1 h.2⟩
diff --git a/Mathlib/Topology/MetricSpace/Contracting.lean b/Mathlib/Topology/MetricSpace/Contracting.lean
@@ -91,6 +91,7 @@ We include more conclusions in this theorem to avoid proving them again later.
 
 The main API for this theorem are the functions `efixedPoint` and `fixedPoint`,
 and lemmas about these functions. -/
+@[wikidata Q220680]
 theorem exists_fixedPoint (hf : ContractingWith K f) (x : α) (hx : edist x (f x) ≠ ∞) :
     ∃ y, IsFixedPt f y ∧ Tendsto (fun n ↦ f^[n] x) atTop (𝓝 y) ∧
       ∀ n : ℕ, edist (f^[n] x) y ≤ edist x (f x) * (K : ℝ≥0∞) ^ n / (1 - K) :=
diff --git a/Mathlib/Topology/Order/IntermediateValue.lean b/Mathlib/Topology/Order/IntermediateValue.lean
@@ -549,6 +549,7 @@ variable {δ : Type*} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopolog
 
 /-- **Intermediate Value Theorem** for continuous functions on closed intervals, case
 `f a ≤ t ≤ f b`. -/
+@[wikidata Q245098]
 theorem intermediate_value_Icc {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Icc a b)) :
     Icc (f a) (f b) ⊆ f '' Icc a b :=
   isPreconnected_Icc.intermediate_value (left_mem_Icc.2 hab) (right_mem_Icc.2 hab) hf
diff --git a/Mathlib/Topology/UrysohnsLemma.lean b/Mathlib/Topology/UrysohnsLemma.lean
@@ -318,6 +318,7 @@ then there exists a continuous function `f : X → ℝ` such that
 * `f` equals one on `t`;
 * `0 ≤ f x ≤ 1` for all `x`.
 -/
+@[wikidata Q1816967]
 theorem exists_continuous_zero_one_of_isClosed [NormalSpace X]
     {s t : Set X} (hs : IsClosed s) (ht : IsClosed t)
     (hd : Disjoint s t) : ∃ f : C(X, ℝ), EqOn f 0 s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 := by
