{"entities":{"P14534":{"pageid":13490,"ns":122,"title":"Property:P14534","lastrevid":13490,"modified":"2026-07-04T12:57:36Z","type":"property","datatype":"external-id","id":"P14534","labels":{"en":{"language":"en","value":"Mathlib Declaration ID"},"fr":{"language":"fr","value":"ID de d\u00e9claration Mathlib"},"ko":{"language":"ko","value":"Mathlib \uc120\uc5b8 ID"},"zh-hans":{"language":"zh-hans","value":"Mathlib \u58f0\u660e ID"},"ca":{"language":"ca","value":"identificador Mathlib de declaraci\u00f3"},"nl":{"language":"nl","value":"Mathlib-identificatiecode voor verklaring"},"de":{"language":"de","value":"Mathlib Deklaration ID"}},"descriptions":{"en":{"language":"en","value":"identifier for a declaration in Mathlib, the mathematics library of the Lean theorem prover, that formalizes this concept"},"fr":{"language":"fr","value":"identifiant pour une d\u00e9claration dans Mathlib, la librairie de math\u00e9matiques du prouveur de th\u00e9or\u00e8mes Lean, qui formalise ce concept"},"ko":{"language":"ko","value":"Lean \uc815\ub9ac \uc99d\uba85 \ub3c4\uad6c\uc758 \uc218\ud559 \ub77c\uc774\ube0c\ub7ec\ub9ac Mathlib\uc5d0\uc11c, \uc774 \uac1c\ub150\uc744 \ud615\uc2dd\ud654\ud558\ub294 \uc120\uc5b8\uc758 \uc2dd\ubcc4\uc790"},"zh-hans":{"language":"zh-hans","value":"Lean \u5b9a\u7406\u8bc1\u660e\u5de5\u5177\u6570\u5b66\u5e93 Mathlib \u4e2d\uff0c\u5f62\u5f0f\u5316\u8fd9\u4e00\u6982\u5ff5\u7684\u58f0\u660e\u7684 ID"},"nl":{"language":"nl","value":"identificatiecode voor een wiskundig concept in de Mathlib-documentatie"},"de":{"language":"de","value":"Identifikator f\u00fcr eine Deklaration in Mathlib, der Mathematikbibliothek des Lean-Beweisassistenten"}},"aliases":{"en":[{"language":"en","value":"Mathlib declaration"},{"language":"en","value":"Mathlib ID"},{"language":"en","value":"Lean declaration"}],"fr":[{"language":"fr","value":"D\u00e9claration Mathlib"},{"language":"fr","value":"ID Mathlib"},{"language":"fr","value":"D\u00e9claration Lean"}],"ko":[{"language":"ko","value":"Mathlib \uc120\uc5b8"},{"language":"ko","value":"Mathlib ID"},{"language":"ko","value":"Lean \uc120\uc5b8"}],"zh-hans":[{"language":"zh-hans","value":"Mathlib \u58f0\u660e"},{"language":"zh-hans","value":"Mathlib ID"},{"language":"zh-hans","value":"Lean \u58f0\u660e"}],"de":[{"language":"de","value":"Mathlib Deklarations-ID"}]},"claims":{}}}}