{"entities":{"Q2819195":{"pageid":2829933,"ns":120,"title":"Item:Q2819195","lastrevid":83585372,"modified":"2026-05-07T09:08:48Z","type":"item","id":"Q2819195","labels":{"en":{"language":"en","value":"Formalizing double groupoids and cross modules in the Lean theorem prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6630639"}},"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":"Q2819195$7BD1BF79-4F95-4043-A41F-C6EDC9396B75","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"81e6e4227be2ecd152c1c3e3c1cd1342030d90be","datavalue":{"value":{"text":"Formalizing Double Groupoids and Cross Modules in the Lean Theorem Prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2819195$38AA43D3-B3B5-4FDC-A51D-876CBA2E29A3","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2976d7ec657a74bc5b0df376bafc7f2f1478ffc9","datavalue":{"value":"1434.68647","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819195$A161FB2C-B0E5-4D66-A2AF-CD732E3290A5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b44779d0f3c17227423972fa92d5f197c3bd9f4f","datavalue":{"value":"10.1007/978-3-319-42432-3_4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819195$C0746EB9-EE9C-4097-AEED-66A7F99812AC","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8ed91f18c49a16f542aacf01077ba8073712fd1e","datavalue":{"value":{"entity-type":"item","numeric-id":1687768,"id":"Q1687768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819195$20ABD8C4-3390-40E9-8A4B-244769F9AF2D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"5ce1d49245d97a30ecabe94a0469a6616f4841aa","datavalue":{"value":{"entity-type":"item","numeric-id":2819192,"id":"Q2819192"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819195$E4740A9B-A386-44C6-B581-E6DA9CE80F9A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"300772c5a0b58bf4f4bfdafa9010450cf2acf8fe","datavalue":{"value":{"time":"+2016-09-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2819195$E6051345-0767-43C5-8FC0-387F3CF7C9EF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819195$D2F81747-707D-4E2F-BBBD-2E31F8ECF949","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2ad0e3e4c8b05ff152d6f7c1973a75cc4fbc9be3","datavalue":{"value":"18G45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819195$8AA6950C-E423-4EF4-9181-45B8A0585CC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40623867f27d5837b7d9156c695c2c009a8863e2","datavalue":{"value":"18G50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819195$09110545-CC6C-4298-A779-E7D267A5AFB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"36d4ee2aca74c4c0df9926d6f3cf4629e4beb1fa","datavalue":{"value":"20L05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819195$74E1FFBE-F3B2-4F94-A59F-EC44F14D36BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819195$CE97BB3B-BCC4-4B51-AABF-D6C853C6C4BE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6764d6e40545bcdef84ea97400da629d59a1896c","datavalue":{"value":"6630639","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819195$E6A45F6C-5F09-4147-ACB9-13F97DD699AB","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"658126897c7f6bf3db78fea48b2876524c1d8c9e","datavalue":{"value":"formalization of mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q2819195$B87E85EE-ACF9-4FEE-BDC9-F94F7ECE4677","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"99edcf085d65da80623477299991b5a5d282b943","datavalue":{"value":"algebraic topology","type":"string"},"datatype":"string"},"type":"statement","id":"Q2819195$EB3432AA-0C7B-40EA-9BB3-9507B047B98D","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":"Q2819195$C0E1582C-F81E-4CC3-8DAD-961976CC76A7","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"33f8fd2cb08aa39020367e826cf835a7b68939b6","datavalue":{"value":"https://doi.org/10.1007/978-3-319-42432-3_4","type":"string"},"datatype":"url"},"type":"statement","id":"Q2819195$73C7B258-7D06-438D-9900-E09C4A81AFC2","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"aa01087688fd5225c3c7820c7f4a4516f4acf237","datavalue":{"value":"W2500686156","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819195$0509CC64-DE93-4D2E-A61E-CD50B2881182","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"38c59c4f1c099bf3aa105699227af5848a751ebc","datavalue":{"value":{"entity-type":"item","numeric-id":636218,"id":"Q636218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819195$1B26F689-BD37-41DB-B03D-1913F8DCD812","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":"Q2819195$817F871B-D2F4-4DCC-9C54-9CED45F73B07","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a611ae37cd77e81d821a59e1af5afe2303c597fc","datavalue":{"value":{"entity-type":"item","numeric-id":1687770,"id":"Q1687770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"955a197c01fa23684359ea10c7f6fd7ffa0d44bd","datavalue":{"value":{"amount":"+0.7585503458976746","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":"Q2819195$EEB481A3-0C8C-48EB-A811-6D5443EA89AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"952dd0313ffcdf0b91b490f0739b8e7d073d048d","datavalue":{"value":{"entity-type":"item","numeric-id":3454108,"id":"Q3454108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7f0ae316abec589e827f6314dbcc6cda75ae1e4b","datavalue":{"value":{"amount":"+0.7259872555732727","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":"Q2819195$E1A96F68-2CE9-4F57-9D48-7992DF70C889","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f46f34e4cc650b64ebb003303883a13e97b05d02","datavalue":{"value":{"entity-type":"item","numeric-id":5145293,"id":"Q5145293"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"254574190a28225350b39af039ed39b6b19a082e","datavalue":{"value":{"amount":"+0.7159984111785889","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":"Q2819195$8442E676-4FD6-497A-8032-3D25B62D41AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2acf841d26e9ea58aed4646059df1014d3f65d19","datavalue":{"value":{"entity-type":"item","numeric-id":5271059,"id":"Q5271059"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ae6391e28b70dd4b4ab5161c38f9454ee9a3df0f","datavalue":{"value":{"amount":"+0.6981712579727173","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":"Q2819195$FFFDAF3F-87DF-4497-B092-0D0E1600838C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dbfc612fa3980070fdd53a2cb4ca179e44861c9c","datavalue":{"value":{"entity-type":"item","numeric-id":2128117,"id":"Q2128117"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a476af9b31fff95dc63bc6ad9286f939cd79dcea","datavalue":{"value":{"amount":"+0.6872737407684326","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":"Q2819195$10ABF52C-5C5C-4574-879C-72D0CE16DD0E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formalizing double groupoids and cross modules in the Lean theorem prover","badges":[]}}}}}