{"entities":{"Q5195277":{"pageid":7224849,"ns":120,"title":"Item:Q5195277","lastrevid":53534390,"modified":"2026-01-25T04:55:27Z","type":"item","id":"Q5195277","labels":{"en":{"language":"en","value":"Implementation of Bourbaki's \\textit{Elements of mathematics} in Coq. II: From natural numbers to real numbers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7106511"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5195277$061F75F9-A464-4664-B60C-D72F992309C4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9c78462069e2c258b7b7bf28d42280c51049ad2a","datavalue":{"value":"1451.68339","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5195277$1253FAF5-A65F-4E2B-B719-F14F281C16F7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9360e45f322d1ba8012d3f5472eb549636095c9c","datavalue":{"value":{"entity-type":"item","numeric-id":1811166,"id":"Q1811166"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5195277$7483BB74-D422-4F9E-86E5-E925F42EEDE2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5e86f4a04633c16a30a7b65e0a3f44b477c2fa3c","datavalue":{"value":{"time":"+2019-09-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5195277$F764F2CB-7A4C-4B1C-8A80-A0FFC56597D0","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5195277$A84E5843-6390-4B85-B8AD-09958CB65D50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5195277$6C021393-0E48-4EA2-952C-1B118222C082","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7d6d1b45c606677a96fadd625efc72a171c20037","datavalue":{"value":"03E99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5195277$B86B3B01-1BD4-4ABB-B999-E3FFD40BA886","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2725800ff5a350141d7e6e92522a13e911fe6742","datavalue":{"value":"7106511","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5195277$ED446300-55FE-4A90-9F52-441DE07FC1AC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q5195277$B7D2F5A8-3C60-46A4-8DC6-B8EA0747D8B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"322f4c491e7b9629a362e3201f4bd868260d92f3","datavalue":{"value":"Bourbaki","type":"string"},"datatype":"string"},"type":"statement","id":"Q5195277$AD132CCD-8ABE-4514-A0A9-F8267673F407","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0429ee50e2d52b97211c82b6623249a62ba21adb","datavalue":{"value":"sets","type":"string"},"datatype":"string"},"type":"statement","id":"Q5195277$E8CF918E-77DC-45FA-9526-B691B659D1D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"19de6affdb1ba772c772b8d14fa3ed4bab919573","datavalue":{"value":"integers","type":"string"},"datatype":"string"},"type":"statement","id":"Q5195277$8F591EE3-BB9E-497E-8B27-399623778C97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ff8b49d4296d1d1bb6a846f657357c3f0aa16481","datavalue":{"value":"rational numbers","type":"string"},"datatype":"string"},"type":"statement","id":"Q5195277$0E635F04-377C-4DE8-95E9-C660227BB0DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"93870bea9e95850a8c2c168e966ba73051e6fe83","datavalue":{"value":"real numbers","type":"string"},"datatype":"string"},"type":"statement","id":"Q5195277$78A1BA77-A118-425F-9BBC-CBE034570D08","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0ee4919dba608fb88895148261fb02ed1a66290c","datavalue":{"value":{"entity-type":"item","numeric-id":21587,"id":"Q21587"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5195277$73C4E694-2875-4B75-9BFF-E342C39FEE5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5195277$1D6B455B-44AB-40B8-93F3-26E8874C42B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a94daa7865c51c0d2412cced8422ea9361d06e30","datavalue":{"value":{"entity-type":"item","numeric-id":21343,"id":"Q21343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5195277$A4C3691F-DD9D-4646-999C-8C818451026F","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5195277$8C399628-05A2-4F3F-8164-B743E0217415","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6801e265573b842b550c756bd60326ad39bef38b","datavalue":{"value":"https://doaj.org/article/b7e37bc9ffcf459692a7c8f59465a3aa","type":"string"},"datatype":"url"},"type":"statement","id":"Q5195277$323B0843-3CB3-4A9B-B235-2E49647413DE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"cd9b8b3758972fc238a104fd718c508a690bc7d0","datavalue":{"value":"W2570826447","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5195277$3A7CCC33-0626-4353-B113-15186EB099B4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ff696368bebd71907a5fabaa8644c2615e12c57b","datavalue":{"value":{"text":"Implementation of Bourbaki's Elements of   Mathematics in Coq:  Part Two, From Natural Numbers to Real Numbers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5195277$A394BB9B-0461-42DB-8B70-EC4173AD26F1","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc90f519741959885c97856c7164fc497d5566b1","datavalue":{"value":{"entity-type":"item","numeric-id":2973239,"id":"Q2973239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5195277$00B467AE-DDC0-45CF-A147-FAD422FF314F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ee900a14eb345f1ec6416bc370340cd0e2c18c0","datavalue":{"value":{"entity-type":"item","numeric-id":5565097,"id":"Q5565097"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5195277$01323522-E9A0-447F-B229-22918556CE8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf2d3988c57102e993e791fa9cf13cfbd751cecc","datavalue":{"value":{"entity-type":"item","numeric-id":4040889,"id":"Q4040889"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5195277$BF8A351A-CA4E-4C70-850C-5D248137CC8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6b00a92b4e0f4a6f2c10346ae58f94938b1b4077","datavalue":{"value":{"entity-type":"item","numeric-id":5522002,"id":"Q5522002"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5195277$E4577D1F-444B-4A04-A394-9FFE8F1521BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a291d4cf6a21f184ed89e23d3d44baace280bb6d","datavalue":{"value":{"entity-type":"item","numeric-id":2914733,"id":"Q2914733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5195277$637F7E39-E598-40EB-93F2-52218272E141","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2a2b1613537d61a815e216e05ccf435cf17616eb","datavalue":{"value":{"entity-type":"item","numeric-id":4117362,"id":"Q4117362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5195277$F02EBAEF-0388-4FFF-BFD4-9BFA51589876","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8c6dee845aa2fb3e3b96fd0f5f996675d409056","datavalue":{"value":{"entity-type":"item","numeric-id":3183538,"id":"Q3183538"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5195277$E92EA462-C837-4A5B-9A67-408187512DE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d43f11a5e6fc21caa581e9ac1e35682b1839d73e","datavalue":{"value":{"entity-type":"item","numeric-id":3075246,"id":"Q3075246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5195277$D47EA245-CD51-4C5D-9921-A007FFFDD03A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9ab2185173b12827e0bf6620188d491b0f53625d","datavalue":{"value":{"entity-type":"item","numeric-id":3075244,"id":"Q3075244"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5195277$6E460472-1F3D-4CB2-96ED-324E09AE271F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5af4924e0bc2cd010b30cb46e8a584460ba0bc2c","datavalue":{"value":{"entity-type":"item","numeric-id":5712314,"id":"Q5712314"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5195277$5A96E610-E794-4D8A-B772-E9914BDB662A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"64e038e175150b20a8ef1df3fda34e490d22d245","datavalue":{"value":{"entity-type":"item","numeric-id":2457309,"id":"Q2457309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5195277$242BBB64-E34F-4809-A448-934828EBC0CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bae36cf3ec702071748ee3693c68abe49d3bcf5f","datavalue":{"value":{"entity-type":"item","numeric-id":704001,"id":"Q704001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5195277$5C7F1F0C-F352-47F1-AFD4-EA748FB73A03","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"faa88573b65d53e480157c9c4814d8faa110ff51","datavalue":{"value":"10.6092/ISSN.1972-5787/4771","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5195277$9F6BAFF2-31CF-46FF-8E67-3CA5AEAD1D46","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"277e7249a69282f954442c61a0a57324c686c3da","datavalue":{"value":{"entity-type":"item","numeric-id":3075244,"id":"Q3075244"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"96157f4bcdb5a861415d1c5b67796411389a2c38","datavalue":{"value":{"amount":"+0.8873881101608276","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5195277$E1034F46-7AA9-41CF-B938-8ACE1627A1EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d82c0eecf42b47cff6f33826f791505c22f670ad","datavalue":{"value":{"entity-type":"item","numeric-id":4736391,"id":"Q4736391"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"caca0416fb087393bf75a89eb0e101fda981d31a","datavalue":{"value":{"amount":"+0.7837676405906677","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5195277$EB64D052-631F-4CAA-83E8-A635DC016810","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0345b8d111ccf35f17db68bc0571366fd7b5303d","datavalue":{"value":{"entity-type":"item","numeric-id":2914733,"id":"Q2914733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1a7e72580a50272ddf270b3fb6dd1463b0d70795","datavalue":{"value":{"amount":"+0.7499735355377197","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5195277$8C0FBFEA-3EF1-4678-A0C5-EDA5E2A7D745","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6ad4c053fd4fe39c501b9b259118832ad25383ee","datavalue":{"value":{"entity-type":"item","numeric-id":2766803,"id":"Q2766803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dfa74cdc2167dea7e16468b3cc9d3773407d82fa","datavalue":{"value":{"amount":"+0.7437744140625","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5195277$5AB7E8F9-7C3D-4E86-AD55-ACEE8CAB5774","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8f9b44095d13cd2bcad82afdc067f0870b5d91e6","datavalue":{"value":{"entity-type":"item","numeric-id":5740657,"id":"Q5740657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fa37e7f896dab06cf966fd7ba3788d565d9ee8fc","datavalue":{"value":{"amount":"+0.7432143688201904","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5195277$B4F2A078-BF24-4E81-8B30-48A7DF3C0279","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5195277","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5195277"}}}}}