[Merged by Bors] - doc: add wikidata attributes by Deicyde · Pull Request #40861 · leanprover-community/mathlib4

Deicyde · 2026-06-21T11:02:07Z

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 and Wikilean.

See https://wikilean.jackmccarthy.org/review?pr=40861 for reviewer UI.

Deicyde · 2026-06-21T11:02:20Z

This PR adds 14 @[wikidata] cross-reference tags.

#	Concept	Wikidata	Mathlib declaration	Reviews
1	Linear recurrence with constant coefficients	Q364089	`LinearRecurrence`	🟢 @SnirBroshi · 🟢 @Deicyde · 🟢 @jcommelin*
2	Euclidean space	Q17295	`EuclideanSpace`	🟢 @SnirBroshi · 🟢 @vihdzp · 🟢 @Deicyde · 🟢 @jcommelin*
3	Basis (linear algebra)	Q189569	`Module.Basis`	🟢 @SnirBroshi · 🟢 @vihdzp · 🟢 @Deicyde · 🟢 @jcommelin*
4	Clifford algebra	Q674689	`CliffordAlgebra`	🟢 @vihdzp · 🟢 @Deicyde · 🟢 @jcommelin*
5	Dual space	Q752487	`Module.Dual`	🟢 @SnirBroshi · 🟢 @vihdzp · 🟢 @Deicyde · 🟢 @jcommelin*
6	Root system	Q534131	`RootPairing.IsRootSystem`	🟢 @vihdzp · 🟢 @Deicyde · 🟢 @jcommelin*
7	Conditional expectation	Q772232	`MeasureTheory.condExp`	🟢 @Deicyde · 🟢 @jcommelin*
8	Integration by substitution	Q1071270	`intervalIntegral.integral_comp_mul_deriv`	🟢 @Deicyde
9	Trapezoidal rule	Q833293	`trapezoidal_integral`	🟢 @Deicyde · 🟢 @jcommelin*
10	Riemann zeta function	Q187235	`riemannZeta`	🟢 @vihdzp · 🟢 @Deicyde · 🟢 @jcommelin*
11	Maximum and minimum	Q845060	`IsExtrOn`	🟢 @Deicyde
12	Residue field	Q7315530	`IsLocalRing.ResidueField`	🟢 @vihdzp · 🟢 @Deicyde · 🟢 @jcommelin*
13	Locally convex topological vector space	Q1572357	`LocallyConvexSpace`	🟢 @vihdzp · 🟢 @Deicyde · 🟢 @jcommelin*
14	Complete metric space	Q848569	`CompleteSpace`	🟢 @SnirBroshi · 🟢 @vihdzp · 🟢 @Deicyde · 🟢 @jcommelin*

_{Reviews: 🟢 approve · 🟡 revise · 🔴 reject · ⚠️ deletion-candidate · 💬 comment. * = maintainer. Recycled tags: https://wikilean.jackmccarthy.org/queue}

Deicyde · 2026-06-21T11:02:22Z

LLM-generated

Deicyde · 2026-06-21T11:02:26Z

+@[wikidata Q1071270]
 theorem integral_comp_mul_deriv {f f' g : ℝ → ℝ} (h : ∀ x ∈ uIcc a b, HasDerivAt f (f' x) x)


Wikidata Q1071270: integration by substitution — method of integration

This looks good, but undergrad.yaml references the SMul version instead: intervalIntegral.integral_deriv_smul_comp. Maybe both should be tagged?

Deicyde · 2026-06-21T11:02:26Z

+@[ext, wikidata Q1206110]
 class Module (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] extends


Wikidata Q1206110: program operator — construct used in computer programming, often associated to a mathematical operation

This looks wrong, should be Q18848

Deicyde · 2026-06-21T11:02:26Z

+@[wikidata Q1365258]
 def fourierIntegral (e : AddChar 𝕜 𝕊) (μ : Measure V) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E)


Wikidata Q1365258: Fourier analysis — branch of mathematics regarding periodic and continuous signals

Deicyde · 2026-06-21T11:02:26Z

+@[wikidata Q1412905]
 abbrev Equiv.Perm (α : Sort*) :=


Wikidata Q1412905: permutation group — group whose operation is composition of permutations

This is subtle, but it should be Q849512 symmetric group instead.
The first paragraph of the Wikipedia article clarifies that a permutation group is a subgroup of the symmetric group, aka Subgroup (Equiv.Perm α).

Furthermore, this should probably be Q161519 permutation, while Equiv.Perm.permGroup should have Q849512 symmetric group.

Deicyde · 2026-06-21T11:02:26Z

+@[wikidata Q1572357]
 class LocallyConvexSpace (𝕜 E : Type*) [Semiring 𝕜] [PartialOrder 𝕜]


Wikidata Q1572357: locally convex space — topological vector space in which every vector has a convex neighborhood

Deicyde · 2026-06-21T11:02:27Z

+@[wikidata Q772232]
 noncomputable irreducible_def condExp (μ : Measure[m₀] α) (f : α → E) : α → E :=


Wikidata Q772232: conditional expectation — expected value in a conditional distribution

Deicyde · 2026-06-21T11:02:27Z

+@[wikidata Q833293]
 noncomputable def trapezoidal_integral (f : ℝ → ℝ) (N : ℕ) (a b : ℝ) : ℝ :=


Wikidata Q833293: trapezoidal rule — numerical integration method

Deicyde · 2026-06-21T11:02:27Z

+@[wikidata Q845060]
 def IsExtrOn : Prop :=


Wikidata Q845060: maxima and minima — largest and smallest value taken by a function in a given range

We also have IsMinOn/IsMaxOn btw

Deicyde · 2026-06-21T11:02:27Z

+@[wikidata Q848569]
 class CompleteSpace (α : Type u) [UniformSpace α] : Prop where


Wikidata Q848569: complete metric space — metric space in which cauchy sequence converges to an element of the space

Deicyde · 2026-06-21T11:02:27Z

+@[wikidata Q938102]
 def weierstrassP (z : ℂ) : ℂ := ∑' l : L.lattice, (1 / (z - l) ^ 2 - 1 / l ^ 2)


Wikidata Q938102: elliptic function — class of mathematical functions

This should probably be Q2343600.
It's an elliptic function, not the concept of it.

github-actions · 2026-06-21T11:03:23Z

PR summary a5971f457f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

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.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit a5971f4).

+0 new declarations
−0 removed declarations

No declaration differences.

No changes to strong technical debt.

No changes to weak technical debt.

Current commit a5971f457f
Reference commit 66255bfc74

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).

jcommelin · 2026-06-22T05:51:39Z

WikiLean review

Q1206110 Operator (computer programming) — Mathlib/Algebra/Module/Defs.lean:54
- status: 🔴 reject
Q364089 Linear recurrence with constant coefficients — Mathlib/Algebra/LinearRecurrence.lean:52
- status: 🟢 approve
Q582659 Exponential growth — Mathlib/Analysis/Asymptotics/ExpGrowth.lean:42
- status: 🔴 reject
Q1365258 Fourier analysis — Mathlib/Analysis/Fourier/FourierTransform.lean:83
- status: 🔴 reject
- This QID refers to a whole subfield of maths, not to one specific concept.
Q17295 Euclidean space — Mathlib/Analysis/InnerProductSpace/PiL2.lean:112
- status: 🟢 approve
Q938102 Elliptic function — Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean:269
- status: 🔴 reject
Q163310 Turing machine — Mathlib/Computability/TuringMachine/PostTuringMachine.lean:135
- The "this" in "this is a deliberate addition, see comment" refers to the unusedArguments attribute. This should now be clarified.
Q189569 Basis (linear algebra) — Mathlib/LinearAlgebra/Basis/Defs.lean:89
- status: 🟢 approve
Q674689 Clifford algebra — Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean:70
- status: 🟢 approve
Q752487 Dual space — Mathlib/LinearAlgebra/Dual/Defs.lean:61
- status: 🟢 approve
Q534131 Root system — Mathlib/LinearAlgebra/RootSystem/Defs.lean:117
- status: 🟢 approve
Q1412905 Permutation group — Mathlib/Logic/Equiv/Defs.lean:99
- status: 🔴 reject
Q772232 Conditional expectation — Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean:101
- status: 🟢 approve
Q833293 Trapezoidal rule — Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean:33
- status: 🟢 approve
Q187235 Riemann zeta function — Mathlib/NumberTheory/LSeries/RiemannZeta.lean:120
- status: 🟢 approve
Q7315530 Residue field — Mathlib/RingTheory/LocalRing/ResidueField/Defs.lean:29
- status: 🟢 approve
Q1572357 Locally convex topological vector space — Mathlib/Topology/Algebra/Module/LocallyConvex.lean:50
- status: 🟢 approve
Q848569 Complete metric space — Mathlib/Topology/UniformSpace/Cauchy.lean:369
- status: 🟢 approve

_{Generated by the WikiLean review tool — review this PR}

Deicyde · 2026-06-22T21:54:26Z


 /-- A "linear recurrence relation" over a commutative semiring is given by its
  order `n` and `n` coefficients. -/
+@[wikidata Q364089]


🟢 WikiLean reviewer note (approve)

(no note)

_Q364089

Deicyde · 2026-06-22T21:54:27Z

  (where `r : R` and `x : M`) with some natural associativity and
  distributivity axioms similar to those on a ring. -/
-@[ext]
+@[ext, wikidata Q1206110]


🔴 WikiLean reviewer note (reject)

(no note)

_Q1206110

Deicyde · 2026-06-22T21:54:28Z

 noncomputable def expGrowthInf (u : ℕ → ℝ≥0∞) : EReal := liminf (fun n ↦ log (u n) / n) atTop

 /-- Upper exponential growth of a sequence of extended nonnegative real numbers. -/
+@[wikidata Q582659]


🔴 WikiLean reviewer note (reject)

(no note)

_Q582659

Deicyde · 2026-06-22T21:54:29Z


 /-- The Fourier transform integral for `f : V → E`, with respect to a bilinear form `L : V × W → 𝕜`
 and an additive character `e`. -/
+@[wikidata Q1365258]


🔴 WikiLean reviewer note (reject)

(no note)

_Q1365258

Deicyde · 2026-06-22T21:54:30Z


 For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
 analogous to `![x, y, ...]` notation. -/
+@[wikidata Q17295]


🟢 WikiLean reviewer note (approve)

(no note)

_Q17295

Deicyde · 2026-06-22T21:54:31Z

 section weierstrassP

 /-- The Weierstrass `℘` function. This has the notation `℘[L]` in the namespace `PeriodPairs`. -/
+@[wikidata Q938102]


🔴 WikiLean reviewer note (reject)

(no note)

_Q938102

Deicyde · 2026-06-22T21:54:31Z

  for `Γ` is the "blank" tape value, and the default value of `Λ` is
  the initial state. -/
-@[nolint unusedArguments] -- this is a deliberate addition, see comment
+@[nolint unusedArguments, wikidata Q163310] -- this is a deliberate addition, see comment


🔴 WikiLean reviewer note (reject)

We should use Pot-Turing Machine (Q2574032) instead

_Q163310

Deicyde · 2026-06-22T21:54:32Z

 They are internally represented as linear equivs `M ≃ₗ[R] (ι →₀ R)`,
 available as `Basis.repr`.
 -/
+@[wikidata Q189569]


🟢 WikiLean reviewer note (approve)

(no note)

_Q189569

Deicyde · 2026-06-22T21:54:33Z


 /-- The Clifford algebra of an `R`-module `M` equipped with a `QuadraticForm` `Q`.
 -/
+@[wikidata Q674689]


🟢 WikiLean reviewer note (approve)

(no note)

_Q674689

Deicyde · 2026-06-22T21:54:34Z

 variable [CommSemiring R] [AddCommMonoid M] [Module R M]

 /-- The left dual space of an R-module M is the R-module of linear maps `M → R`. -/
+@[wikidata Q752487]


🟢 WikiLean reviewer note (approve)

(no note)

_Q752487

Deicyde · 2026-06-22T21:54:35Z

 variable (P : RootPairing ι R M N) (i j : ι)

 /-- A root system is a root pairing for which the roots and coroots span their ambient modules. -/
+@[wikidata Q534131]


🟢 WikiLean reviewer note (approve)

(no note)

_Q534131

Deicyde · 2026-06-22T21:54:36Z

  ⟨EquivLike.toEquiv⟩

 /-- `Perm α` is the type of bijections from `α` to itself. -/
+@[wikidata Q1412905]


🔴 WikiLean reviewer note (reject)

Use Q161519 instead

_Q1412905

Deicyde · 2026-06-22T21:54:37Z

 - `m` is not a sub-σ-algebra of `m₀`,
 - `μ` is not σ-finite with respect to `m`,
 - `f` is not integrable. -/
+@[wikidata Q772232]


🟢 WikiLean reviewer note (approve)

(no note)

_Q772232

Deicyde · 2026-06-22T21:54:38Z

 and `g` is continuous, then we can substitute `u = f x` to get
 `∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u`.
 -/
+@[wikidata Q1071270]


🟢 WikiLean reviewer note (approve)

I agree, with Snir, let's tag intervalIntegral.integral_deriv_smul_comp as well

_Q1071270

Deicyde · 2026-06-22T21:54:38Z

 /-- Integration of `f` from `a` to `b` using the trapezoidal rule with `N+1` total evaluations of
 `f`.  (Note the off-by-one problem here: `N` counts the number of trapezoids, not the number of
 evaluations.) -/
+@[wikidata Q833293]


🟢 WikiLean reviewer note (approve)

(no note)

_Q833293

Deicyde · 2026-06-22T21:54:39Z

 -/

 /-- The Riemann zeta function `ζ(s)`. -/
+@[wikidata Q187235]


🟢 WikiLean reviewer note (approve)

(no note)

_Q187235

Deicyde · 2026-06-22T21:54:40Z

  IsMaxFilter f (𝓟 s) a

 /-- `IsExtrOn f s a` means `IsMinOn f s a` or `IsMaxOn f s a` -/
+@[wikidata Q845060]


🟢 WikiLean reviewer note (approve)

We should also look into Q1076611 limit inferior and limit superior

_Q845060

Deicyde · 2026-06-22T21:54:41Z

 /-- The `ℝ`-valued variance of a real-valued random variable defined by applying `ENNReal.toReal`
 to `evariance`. -/
-@[wikidata Q175199]
+@[wikidata Q175199, wikidata Q159375]


🔴 WikiLean reviewer note (reject)

Already exists. I will fix the script.

_Q175199

Deicyde · 2026-06-22T21:54:42Z


 /-- A `Filtration` on a measurable space `Ω` with σ-algebra `m` is a monotone
 sequence of sub-σ-algebras of `m`. -/
+@[wikidata Q176737]


🔴 WikiLean reviewer note (reject)

"Stochastic process" is too broad. Instead we want filtration (Q55647796)

_Q176737

Deicyde · 2026-06-22T21:54:43Z

 variable (R : Type*) [CommRing R] [IsLocalRing R]

 /-- The residue field of a local ring is the quotient of the ring by its maximal ideal. -/
+@[wikidata Q7315530]


🟢 WikiLean reviewer note (approve)

(no note)

_Q7315530

Deicyde · 2026-06-22T21:54:44Z

  inv_mem' _ := by simp_all only [Set.mem_setOf_eq, inv_pow, inv_one]

-@[simp]
+@[simp, wikidata Q756747]


🔴 WikiLean reviewer note (reject)

Also make sure we are tagging the complex roots of unity, since that is what is described in the Wikidata item

_Q756747

Deicyde · 2026-06-22T21:54:45Z

  defined as the quotient of `Type u` by existence of an equivalence
  (a bijection with explicit inverse). -/
-@[pp_with_univ, wikidata Q163875]
+@[pp_with_univ, wikidata Q163875, wikidata Q4049983]


🔴 WikiLean reviewer note (reject)

(no note)

_Q163875

Deicyde · 2026-06-22T21:54:46Z


 /-- A `LocallyConvexSpace` is a topological semimodule over an ordered semiring in which convex
 neighborhoods of a point form a neighborhood basis at that point. -/
+@[wikidata Q1572357]


🟢 WikiLean reviewer note (approve)

(no note)

_Q1572357

Deicyde · 2026-06-22T21:54:46Z


 /-- A complete space is defined here using uniformities. A uniform space
  is complete if every Cauchy filter converges. -/
+@[wikidata Q848569]


🟢 WikiLean reviewer note (approve)

(no note)

_Q848569

Deicyde · 2026-06-22T21:54:47Z

Reviewed by @Deicyde. Added 24 inline comments, including 7 status changes.

jcommelin · 2026-06-23T15:32:21Z

Thanks 🎉

bors merge

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=40861 for reviewer UI. Co-authored-by: wikilean-bot <bot@wikilean.jackmccarthy.org>

mathlib-bors · 2026-06-23T16:24:47Z

Pull request successfully merged into master.

Build succeeded:

Deicyde commented Jun 21, 2026

View reviewed changes

github-actions Bot added the LLM-generated PRs with substantial input from LLMs - review accordingly label Jun 21, 2026

faenuccio added the documentation Improvements or additions to documentation label Jun 21, 2026

Deicyde commented Jun 22, 2026

View reviewed changes

github-actions Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 22, 2026

doc: add wikidata attributes

f903e97

Deicyde force-pushed the wikilean/wikidata-batch-4 branch from 4e30afe to f903e97 Compare June 23, 2026 03:33

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 23, 2026

Merge branch 'master' into wikilean/wikidata-batch-4

a5971f4

mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label Jun 23, 2026

mathlib-bors Bot changed the title ~~doc: add wikidata attributes~~ [Merged by Bors] - doc: add wikidata attributes Jun 23, 2026

mathlib-bors Bot closed this Jun 23, 2026

		@[wikidata Q1071270]
		theorem integral_comp_mul_deriv {f f' g : ℝ → ℝ} (h : ∀ x ∈ uIcc a b, HasDerivAt f (f' x) x)

		@[ext, wikidata Q1206110]
		class Module (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] extends

		@[wikidata Q1365258]
		def fourierIntegral (e : AddChar 𝕜 𝕊) (μ : Measure V) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E)

		@[wikidata Q1572357]
		class LocallyConvexSpace (𝕜 E : Type*) [Semiring 𝕜] [PartialOrder 𝕜]

		@[wikidata Q772232]
		noncomputable irreducible_def condExp (μ : Measure[m₀] α) (f : α → E) : α → E :=

		@[wikidata Q833293]
		noncomputable def trapezoidal_integral (f : ℝ → ℝ) (N : ℕ) (a b : ℝ) : ℝ :=

		@[wikidata Q848569]
		class CompleteSpace (α : Type u) [UniformSpace α] : Prop where

		@[wikidata Q938102]
		def weierstrassP (z : ℂ) : ℂ := ∑' l : L.lattice, (1 / (z - l) ^ 2 - 1 / l ^ 2)

Conversation

Deicyde commented Jun 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Deicyde commented Jun 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Deicyde commented Jun 21, 2026

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!

SnirBroshi Jun 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

SnirBroshi Jun 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

PR summary a5971f457f

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

jcommelin commented Jun 22, 2026

WikiLean review

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!

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

Deicyde commented Jun 21, 2026 •

edited

Loading

Deicyde commented Jun 21, 2026 •

edited

Loading

SnirBroshi Jun 21, 2026 •

edited

Loading

SnirBroshi Jun 21, 2026 •

edited

Loading

github-actions Bot commented Jun 21, 2026 •

edited

Loading