{"entities":{"Q7323647":{"pageid":31355080,"ns":120,"title":"Item:Q7323647","lastrevid":105121870,"modified":"2026-09-17T13:17:20Z","type":"item","id":"Q7323647","labels":{"en":{"language":"en","value":"A formalization of divided powers in lean"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8249881"}},"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":"Q7323647$81CEDFC7-8010-415A-921A-F43981C7A54A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"efd45caef37c086f35ec1b70807cf275bb0c70f2","datavalue":{"value":{"text":"A formalization of divided powers in lean","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7323647$ED0ECE2E-66E8-4E0A-91D3-908C14FB46D2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"280499bbdccced2b60a89e7095574da2ba837a27","datavalue":{"value":"10.4230/LIPICS.ITP.2025.4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7323647$C50D79C1-1D67-48CB-BACA-AD90F60C39FE","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fba68b73e4c3c2e96c1d329d34959ec147b28519","datavalue":{"value":{"entity-type":"item","numeric-id":167114,"id":"Q167114"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323647$2EADB7F7-BF22-4025-830B-3F824F893880","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9ceb4b13b2876fcca290c6e84e42d1f1c9830cb5","datavalue":{"value":{"entity-type":"item","numeric-id":2086411,"id":"Q2086411"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323647$00845C02-F143-4157-A1AF-9D99019C8C22","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"327bdfdabaae2e8cbc884e8efa23d5004f5f8802","datavalue":{"value":{"time":"+2026-09-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7323647$71265991-5154-431B-80BE-60C47EF9FC5D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7323647$2B7F2FAA-8535-476F-9588-5AEE87DB0DC1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4474b2914301e18f2c9afcbb7f8fc8318218e557","datavalue":{"value":"8249881","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7323647$0B4F2322-0021-4A15-BA0B-B91F952994C9","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323647$1236383A-9FCD-4A89-9499-E9E40397CF8A","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":"Q7323647$3287DE5A-A1DD-4F31-89E9-5296CD6A54E9","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"debf8c29b43ec61022715495da6b1e2000fae350","datavalue":{"value":{"entity-type":"item","numeric-id":1214467,"id":"Q1214467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323647$769FBEA6-8FC6-4661-A514-9B4C925ABA11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5614b6f2a25c7606acd8d5f83e150adebc54481e","datavalue":{"value":{"entity-type":"item","numeric-id":4163626,"id":"Q4163626"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323647$559F8868-3EDD-42E8-925D-9419F268EB80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a55447afe9e55109d21f7cb3e3fc40d677697651","datavalue":{"value":{"entity-type":"item","numeric-id":5891671,"id":"Q5891671"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323647$E89984C4-9D2D-452A-AD30-F6E4A4D0CDCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"10d5a78d748108c26d72c564e55c5a3af97fca93","datavalue":{"value":{"entity-type":"item","numeric-id":6642992,"id":"Q6642992"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323647$E3B1086B-F38A-4631-B398-6F80320A792E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8242928870aab67343ad0152eb7ca8357168f7f3","datavalue":{"value":{"entity-type":"item","numeric-id":3454108,"id":"Q3454108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323647$44E42EF1-9E32-460F-9BA3-7CF0B37F9363","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"432347ebf7758fa5347be4c601bf2d08f68cb652","datavalue":{"value":{"entity-type":"item","numeric-id":2055901,"id":"Q2055901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323647$334FEA19-5BCE-47E7-AB74-FB5503A2CA01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b6abe9bd707210c9174d9297448b125deb30e7b6","datavalue":{"value":{"entity-type":"item","numeric-id":5740654,"id":"Q5740654"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323647$118F9A03-9A73-47A4-BF1D-AE1328F16206","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8d89ba1f93f46798a88610e299fe84dbb51539d","datavalue":{"value":{"entity-type":"item","numeric-id":5726727,"id":"Q5726727"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323647$C91152F6-C022-4B15-A8FF-F6D5C03DD3D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e77378c30e120dab0bf7fd7f4c5d7744827d1880","datavalue":{"value":{"entity-type":"item","numeric-id":5521581,"id":"Q5521581"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323647$340D7465-6E1A-474F-8CE0-C594AB5FDBE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"15216956946f4b09fa4e63a202efa0dba6fbace9","datavalue":{"value":{"entity-type":"item","numeric-id":5522306,"id":"Q5522306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323647$E0BE638F-72BA-45EE-B656-A6B857418B0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec326779be5f4f8dc3a81efc985f00f310bbe46b","datavalue":{"value":{"entity-type":"item","numeric-id":597122,"id":"Q597122"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7323647$AAC7443C-0039-497E-AC72-F132110EB835","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A formalization of divided powers in lean","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_formalization_of_divided_powers_in_lean"}}}}}