Mathlib Declaration ID

identifier for a declaration in Mathlib, the mathematics library of the Lean theorem prover, that formalizes this concept
rdfs:label
"Mathlib Declaration ID"@en
skos:altLabel
"Lean declaration"@en
"Mathlib ID"@en
"Mathlib declaration"@en
schema:description
"identifier for a declaration in Mathlib, the mathematics library of the Lean theorem prover, that formalizes this concept"@en
schema:dateModified "2026-07-04T12:57:36+00:00"^^xsd:dateTime
schema:version 2513804184
wikibase:claim p:P14534
wikibase:directClaim wdt:P14534
wikibase:directClaimNormalized p:direct-normalized/P14534
wikibase:novalue p:novalue/P14534
wikibase:propertyType wikibase:ExternalId
wikibase:qualifier p:qualifier/P14534
wikibase:qualifierValue p:qualifier/value/P14534
wikibase:qualifierValueNormalized p:qualifier/value-normalized/P14534
wikibase:reference p:reference/P14534
wikibase:referenceValue p:reference/value/P14534
wikibase:referenceValueNormalized p:reference/value-normalized/P14534
wikibase:statementProperty p:statement/P14534
wikibase:statementValue p:statement/value/P14534
wikibase:statementValueNormalized p:statement/value-normalized/P14534
wikibase:statements 21
p:P1630 wd:statement/P14534-272AF841-0A04-4171-B5C3-DA5E84BCC63B
p:P1659 wd:statement/P14534-011FBEE9-7128-4AAD-A9A2-42574E5FA749
wd:statement/P14534-7FFF0927-E73C-4FD3-A880-5522076255A4
wd:statement/P14534-9DD3C31E-E453-4C9C-9F62-3D2BDBF7EDBC
wd:statement/P14534-AB446E28-ED68-43CD-9B69-1132420B10A7
p:P1793 wd:statement/P14534-4AAA4AB8-BAC9-4A4E-9AA7-5804A5619E7E
p:P1855 wd:statement/P14534-1a349c4b-3d27-4d83-8af2-03babb4789a5
wd:statement/P14534-42ca4513-c3fc-478d-a6f4-c85dfc8b6170
wd:statement/P14534-b196ab3d-04c0-4453-a60e-dc838c9e985f
wd:statement/P14534-df6ad152-71d3-4d03-90e0-5c9c67c16eaa
p:P1896 wd:statement/P14534-97460E62-2B23-4086-BEAA-03C086243590
p:P2302 wd:statement/P14534-0E13BD01-2186-4FAE-8248-A5E51ADACAD1
wd:statement/P14534-4B950046-DDAF-48D1-8F2D-D6A9BFF2E36D
wd:statement/P14534-E84B5527-6021-4012-8ED8-7767E06C2D36
wd:statement/P14534-EBFF03F4-498F-4396-8255-CEC966186957
p:P2429 wd:statement/P14534-C17D7030-6FDF-43C1-97C3-150A6B9FDC69
p:P31 wd:statement/P14534-5C6A56FD-AB45-463E-BF2B-F95625A436BD
wd:statement/P14534-77280374-A90D-483C-828B-2CE1083C2E5A
p:P3254 wd:statement/P14534-0DD5EDC5-E782-41BF-B9F9-C3ADB5CBBD91
p:P6104 wd:statement/P14534-45C0069C-0A9B-4B7D-B2B3-E24BC41E4F83
p:P9073 wd:statement/P14534-4698C214-A9B1-491A-8218-1993E6DF66A7
wdt:P1630 "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=$1#doc"
wdt:P1659 Metamath statement ID
MathWorld ID
nLab ID
ProofWiki ID
wdt:P1793 "[\p{L}_][\p{L}\p{N}_'.!?]*"
wdt:P1855 complex number
Cayley's theorem
fundamental theorem of algebra
prime ideal
wdt:P1896 <https://github.com/leanprover-community/mathlib4>
wdt:P2302 format constraint
subject type constraint
allowed-entity-types constraint
property scope constraint
wdt:P2429 always incomplete
wdt:P31 Wikidata property for an identifier
Wikidata property related to mathematics
wdt:P3254 <https://www.wikidata.org/wiki/Wikidata:Property_proposal/Mathlib_declaration_ID>
wdt:P6104 WikiProject Mathematics
wdt:P9073 Mathlib
Download as:
TurtleJSON-LDRDF/XML
data from SPARQL profile: Wikidata