doc: add wikidata attributes (leanprover-community#40682)

Deicyde · bryangingechen · commit b8dedbf69483 · 2026-06-21T20:54:34.000-04:00
This PR adds a batch of 25 `@[wikidata]` attributes. Claude helped generate the list of crossrefs (by scanning Wikidata + Mathlib). Comments are generated by [crossref-report](https://github.com/jcommelin/mathlib-crossref-report) and Wikilean. See https://wikilean.jackmccarthy.org/review?pr=40682 for reviewer UI.
diff --git a/Mathlib/Combinatorics/SimpleGraph/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Basic.lean
@@ -11,6 +11,7 @@ public import Mathlib.Data.Rel
 public import Mathlib.Data.Set.Finite.Basic
 public import Mathlib.Data.Sym.Sym2
 public import Mathlib.Order.CompleteBooleanAlgebra
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # Simple graphs
@@ -88,7 +89,7 @@ The relation describes which pairs of vertices are adjacent.
 There is exactly one edge for every pair of adjacent vertices;
 see `SimpleGraph.edgeSet` for the corresponding edge set.
 -/
-@[ext, aesop safe constructors (rule_sets := [SimpleGraph])]
+@[ext, aesop safe constructors (rule_sets := [SimpleGraph]), wikidata Q141488]
 structure SimpleGraph (V : Type u) where
   /-- The adjacency relation of a simple graph. -/
   Adj : V → V → Prop
diff --git a/Mathlib/Data/Countable/Defs.lean b/Mathlib/Data/Countable/Defs.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Data.Finite.Defs
 public import Mathlib.Data.Bool.Basic
 public import Mathlib.Data.Subtype
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Tactic.MkIffOfInductiveProp
 
 /-!
@@ -36,7 +37,7 @@ variable {α : Sort u} {β : Sort v}
 -/
 
 /-- A type `α` is countable if there exists an injective map `α → ℕ`. -/
-@[mk_iff countable_iff_exists_injective]
+@[mk_iff countable_iff_exists_injective, wikidata Q66707394]
 class Countable (α : Sort u) : Prop where
   /-- A type `α` is countable if there exists an injective map `α → ℕ`. -/
   exists_injective_nat' : ∃ f : α → ℕ, Injective f
diff --git a/Mathlib/Geometry/Manifold/IsManifold/Basic.lean b/Mathlib/Geometry/Manifold/IsManifold/Basic.lean
@@ -10,6 +10,7 @@ public import Mathlib.Analysis.Normed.Module.Convex
 public import Mathlib.Analysis.RCLike.TangentCone
 public import Mathlib.Data.Bundle
 public import Mathlib.Geometry.Manifold.HasGroupoid
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # `C^n` manifolds (possibly with boundary or corners)
@@ -1070,6 +1071,7 @@ variable (M) in
 -- is empty if the base manifold is empty
 /-- The tangent bundle to a manifold, as a Sigma type. Defined in terms of
 `Bundle.TotalSpace` to be able to put a suitable topology on it. -/
+@[wikidata Q746550]
 abbrev TangentBundle := Bundle.TotalSpace E (TangentSpace I : M → Type _)
 
 end TangentSpace
diff --git a/Mathlib/GroupTheory/Solvable.lean b/Mathlib/GroupTheory/Solvable.lean
@@ -10,6 +10,7 @@ public import Mathlib.GroupTheory.Abelianization.Defs
 public import Mathlib.GroupTheory.Perm.ViaEmbedding
 public import Mathlib.GroupTheory.Subgroup.Simple
 public import Mathlib.SetTheory.Cardinal.Order
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # Solvable Groups
@@ -102,7 +103,7 @@ variable (G)
 
 /-- A group `G` is solvable if its derived series is eventually trivial. We use this definition
   because it's the most convenient one to work with. -/
-@[mk_iff isSolvable_def]
+@[mk_iff isSolvable_def, wikidata Q759832]
 class IsSolvable : Prop where
   /-- A group `G` is solvable if its derived series is eventually trivial. -/
   solvable : ∃ n : ℕ, derivedSeries G n = ⊥
diff --git a/Mathlib/LinearAlgebra/Matrix/Defs.lean b/Mathlib/LinearAlgebra/Matrix/Defs.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Module.Pi
 public import Mathlib.Logic.Nontrivial.Basic
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # Matrices
@@ -50,6 +51,7 @@ universe u u' v w
 
 /-- `Matrix m n R` is the type of matrices with entries in `R`, whose rows are indexed by `m`
 and whose columns are indexed by `n`. -/
+@[wikidata Q44337]
 def Matrix (m : Type u) (n : Type u') (α : Type v) : Type max u u' v :=
   m → n → α
 
diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Defs.lean b/Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Data.Set.Countable
 public import Mathlib.Order.ConditionallyCompleteLattice.Basic
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Tactic.FunProp.Attr
 public import Mathlib.Tactic.Measurability
 
@@ -489,7 +490,7 @@ end MeasurableSpace
 
 /-- A function `f` between measurable spaces is measurable if the preimage of every
   measurable set is measurable. -/
-@[fun_prop]
+@[fun_prop, wikidata Q516776]
 def Measurable [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : Prop :=
   ∀ ⦃t : Set β⦄, MeasurableSet t → MeasurableSet (f ⁻¹' t)
 
diff --git a/Mathlib/NumberTheory/DirichletCharacter/Basic.lean b/Mathlib/NumberTheory/DirichletCharacter/Basic.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Group.EvenFunction
 public import Mathlib.Data.ZMod.Units
 public import Mathlib.NumberTheory.MulChar.Basic
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # Dirichlet Characters
@@ -35,6 +36,7 @@ dirichlet character, multiplicative character
 -/
 
 /-- The type of Dirichlet characters of level `n`. -/
+@[wikidata Q1063579]
 abbrev DirichletCharacter (R : Type*) [CommMonoidWithZero R] (n : ℕ) := MulChar (ZMod n) R
 
 open MulChar
diff --git a/Mathlib/NumberTheory/LSeries/RiemannZeta.lean b/Mathlib/NumberTheory/LSeries/RiemannZeta.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.NumberTheory.LSeries.HurwitzZeta
 public import Mathlib.Analysis.PSeriesComplex
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # Definition of the Riemann zeta function
@@ -179,6 +180,7 @@ theorem riemannZeta_one_sub {s : ℂ} (hs : ∀ n : ℕ, s ≠ -n) (hs' : s ≠
 
 /-- A formal statement of the **Riemann hypothesis** – constructing a term of this type is worth a
 million dollars. -/
+@[wikidata Q205966]
 def RiemannHypothesis : Prop :=
   ∀ (s : ℂ) (_ : riemannZeta s = 0) (_ : ¬∃ n : ℕ, s = -2 * (n + 1)) (_ : s ≠ 1), s.re = 1 / 2
 
diff --git a/Mathlib/NumberTheory/Padics/PadicNumbers.lean b/Mathlib/NumberTheory/Padics/PadicNumbers.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.RingTheory.Valuation.Basic
 public import Mathlib.NumberTheory.Padics.PadicNorm
 public import Mathlib.Analysis.Normed.Field.Lemmas
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Tactic.Peel
 public import Mathlib.Topology.MetricSpace.Ultra.Basic
 
@@ -526,6 +527,7 @@ end PadicSeq
 
 /-- The `p`-adic numbers `ℚ_[p]` are the Cauchy completion of `ℚ` with respect to the `p`-adic norm.
 -/
+@[wikidata Q311627]
 def Padic (p : ℕ) [Fact p.Prime] :=
   CauSeq.Completion.Cauchy (padicNorm p)
 deriving Zero, One, Add, Neg, Sub, Mul, Div, AddCommGroup, Ring, CommRing, Field, Inhabited
diff --git a/Mathlib/NumberTheory/Real/Irrational.lean b/Mathlib/NumberTheory/Real/Irrational.lean
@@ -10,6 +10,7 @@ public import Mathlib.Data.Nat.Prime.Int
 public import Mathlib.Data.Rat.Sqrt
 public import Mathlib.Analysis.Real.Sqrt
 public import Mathlib.RingTheory.Algebraic.Basic
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Tactic.IntervalCases
 
 /-!
@@ -32,6 +33,7 @@ but this only works if you `unseal Nat.sqrt.iter in` before the theorem where yo
 open Rat Real
 
 /-- A real number is irrational if it is not equal to any rational number. -/
+@[wikidata Q607728]
 def Irrational (x : ℝ) :=
   x ∉ Set.range ((↑) : ℚ → ℝ)
 
diff --git a/Mathlib/Probability/CDF.lean b/Mathlib/Probability/CDF.lean
@@ -6,6 +6,7 @@ Authors: Rémy Degenne
 module
 
 public import Mathlib.Probability.Kernel.Disintegration.CondCDF
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # Cumulative distribution function of a real probability measure
@@ -51,6 +52,7 @@ namespace ProbabilityTheory
 /-- Cumulative distribution function of a real measure. The definition currently makes sense only
 for probability measures. In that case, it satisfies `cdf μ x = μ.real (Iic x)` (see
 `ProbabilityTheory.cdf_eq_real`). -/
+@[wikidata Q386228]
 noncomputable
 def cdf (μ : Measure ℝ) : StieltjesFunction ℝ :=
   condCDF ((dirac Unit.unit).prod μ) Unit.unit
diff --git a/Mathlib/Probability/Distributions/Gaussian/Real.lean b/Mathlib/Probability/Distributions/Gaussian/Real.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
 public import Mathlib.Probability.HasLaw
 public import Mathlib.Probability.Moments.MGFAnalytic
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # Gaussian distributions over ℝ
@@ -216,6 +217,7 @@ end GaussianPDF
 section GaussianReal
 
 /-- A Gaussian distribution on `ℝ` with mean `μ` and variance `v`. -/
+@[wikidata Q133871]
 noncomputable
 def gaussianReal (μ : ℝ) (v : ℝ≥0) : Measure ℝ :=
   if v = 0 then Measure.dirac μ else volume.withDensity (gaussianPDF μ v)
diff --git a/Mathlib/Probability/Distributions/Poisson/Basic.lean b/Mathlib/Probability/Distributions/Poisson/Basic.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
 public import Mathlib.Probability.HasLaw
 public import Mathlib.Probability.ProbabilityMassFunction.Basic
+public import Mathlib.Tactic.CrossRefAttribute
 
 import Mathlib.LinearAlgebra.Complex.FiniteDimensional
 
@@ -35,6 +36,7 @@ open scoped NNReal Nat
 namespace ProbabilityTheory
 
 /-- The poisson measure with rate `r : ℝ≥0` as a measure over `ℕ`. -/
+@[wikidata Q205692]
 noncomputable
 def poissonMeasure (r : ℝ≥0) : Measure ℕ :=
   Measure.sum (fun n ↦ ENNReal.ofReal (exp (-r) * r ^ n / (n)!) • (.dirac n))
diff --git a/Mathlib/RingTheory/Coprime/Basic.lean b/Mathlib/RingTheory/Coprime/Basic.lean
@@ -11,6 +11,7 @@ public import Mathlib.Algebra.GroupWithZero.Associated
 public import Mathlib.Algebra.Ring.Divisibility.Basic
 public import Mathlib.Algebra.Ring.Hom.Defs
 public import Mathlib.Logic.Basic
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Tactic.Ring
 
 /-!
@@ -40,6 +41,7 @@ variable {R : Type u} [CommSemiring R] (x y z w : R)
 /-- The proposition that `x` and `y` are coprime, defined to be the existence of `a` and `b` such
 that `a * x + b * y = 1`. Note that elements with no common divisors are not necessarily coprime,
 e.g., the multivariate polynomials `x₁` and `x₂` are not coprime. -/
+@[wikidata Q104752]
 def IsCoprime : Prop :=
   ∃ a b, a * x + b * y = 1
 
diff --git a/Mathlib/RingTheory/PowerSeries/Basic.lean b/Mathlib/RingTheory/PowerSeries/Basic.lean
@@ -9,6 +9,7 @@ public import Mathlib.Algebra.CharP.Defs
 public import Mathlib.Algebra.Polynomial.AlgebraMap
 public import Mathlib.Algebra.Polynomial.Basic
 public import Mathlib.RingTheory.MvPowerSeries.Basic
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Tactic.MoveAdd
 public import Mathlib.Algebra.MvPolynomial.Equiv
 public import Mathlib.RingTheory.Ideal.Basic
@@ -55,6 +56,7 @@ noncomputable section
 open Finset (antidiagonal mem_antidiagonal)
 
 /-- Formal power series over a coefficient type `R` -/
+@[wikidata Q1003025]
 abbrev PowerSeries (R : Type*) :=
   MvPowerSeries Unit R
 
diff --git a/Mathlib/Topology/Defs/Basic.lean b/Mathlib/Topology/Defs/Basic.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Order.SetNotation
 public import Mathlib.Tactic.Continuity
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Tactic.FunProp
 public import Mathlib.Tactic.MkIffOfInductiveProp
 public import Mathlib.Data.Nat.Notation
@@ -90,6 +91,7 @@ section Defs
 variable [TopologicalSpace X] [TopologicalSpace Y] {s t : Set X}
 
 /-- `IsOpen s` means that `s` is open in the ambient topological space on `X` -/
+@[wikidata Q213363]
 def IsOpen : Set X → Prop := TopologicalSpace.IsOpen
 
 @[simp] theorem isOpen_univ : IsOpen (univ : Set X) := TopologicalSpace.isOpen_univ
@@ -148,7 +150,7 @@ def DenseRange {α : Type*} (f : α → X) := Dense (range f)
 
 /-- A function between topological spaces is continuous if the preimage
   of every open set is open. Registered as a structure to make sure it is not unfolded by Lean. -/
-@[fun_prop]
+@[fun_prop, wikidata Q170058]
 structure Continuous (f : X → Y) : Prop where
   /-- The preimage of an open set under a continuous function is an open set. Use `IsOpen.preimage`
   instead. -/
diff --git a/Mathlib/Topology/MetricSpace/Pseudo/Defs.lean b/Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Data.ENNReal.Real
 public import Mathlib.Tactic.Bound.Attribute
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Topology.Bornology.Basic
 public import Mathlib.Topology.EMetricSpace.Defs
 public import Mathlib.Topology.UniformSpace.Basic
@@ -365,6 +366,7 @@ namespace Metric
 variable {x y z : α} {δ ε ε₁ ε₂ : ℝ} {s : Set α}
 
 /-- `ball x ε` is the set of all points `y` with `dist y x < ε` -/
+@[wikidata Q838611]
 def ball (x : α) (ε : ℝ) : Set α :=
   { y | dist y x < ε }
 
diff --git a/Mathlib/Topology/UniformSpace/UniformConvergence.lean b/Mathlib/Topology/UniformSpace/UniformConvergence.lean
@@ -5,6 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 module
 
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Topology.UniformSpace.Cauchy
 
 /-!
@@ -110,6 +111,7 @@ theorem tendstoUniformlyOn_iff_tendsto :
 /-- A sequence of functions `Fₙ` converges uniformly to a limiting function `f` with respect to a
 filter `p` if, for any entourage of the diagonal `u`, one has `p`-eventually
 `(f x, Fₙ x) ∈ u` for all `x`. -/
+@[wikidata Q1411887]
 def TendstoUniformly (F : ι → α → β) (f : α → β) (p : Filter ι) :=
   ∀ u ∈ 𝓤 β, ∀ᶠ n in p, ∀ x : α, (f x, F n x) ∈ u
 
