{"entities":{"Q1961914":{"pageid":1972656,"ns":120,"title":"Item:Q1961914","lastrevid":47436700,"modified":"2026-01-01T18:13:54Z","type":"item","id":"Q1961914","labels":{"en":{"language":"en","value":"A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1394789"}},"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":"Q1961914$6CB7C8B3-63AA-4FD4-BC90-E6D7ABE83D78","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5a4f35996747b54cdd559f45cae3215ad10abc33","datavalue":{"value":{"text":"A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1961914$60B885DF-FF9F-43C7-AF1F-8CC85E554440","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e9f7dcc7417804f5879b75cb5e92efcf5323f331","datavalue":{"value":"0943.68149","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961914$7C71AFAF-7F53-4963-91E7-61709DD1E2AB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a2df0c3883277d9e25f44d860aa3a0d951162b31","datavalue":{"value":"10.1023/A:1006269330992","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961914$EC813E35-EC7F-447F-B869-4972ECC1A639","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5be5440cea38e13b33c53cbe578c9b791d6ae808","datavalue":{"value":{"entity-type":"item","numeric-id":433338,"id":"Q433338"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961914$1927D167-4220-450E-8A7B-14C377DDB5EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb5dfbdfa6d8a2070a67ff948fb8abd387eda36e","datavalue":{"value":{"entity-type":"item","numeric-id":352969,"id":"Q352969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961914$7463BEE0-A942-4665-AEA5-F09B37A7F865","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961914$B96AE17E-90C4-4EB8-8477-5C28FF6130E4","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"54c596ed21215ef22823e913d0a98c57f11e119f","datavalue":{"value":{"time":"+2000-09-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1961914$996068B2-EC24-4CD0-9DD2-01D5C9740884","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961914$587CCE4C-448D-4413-9E22-A4BAFD8768E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961914$337944FA-B4DB-4248-BDF8-6888B4A9B33A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ea37469d91f3037e8b6809fc66f770f1b27a461d","datavalue":{"value":"20E07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961914$647E3B35-DCC8-4A3A-B6FA-14FDABE8BFDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f96720fe29e309c34c82deec20bd95823bb71652","datavalue":{"value":"20-04","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961914$66E0F427-AC6D-49A3-A52D-41206FE146E3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"bdb775bd763f60a889e3b5e2aca0d21829989b5d","datavalue":{"value":"1394789","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961914$6EA0AC87-5B18-48A5-AC9F-F844FF4C9931","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4edb23a2ecf41969d4d767eb952fa9304fb6e000","datavalue":{"value":"Isabelle HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q1961914$E57A9D09-E577-42A0-8318-BDC5E0A2C2FC","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b799da0cc0efb29a46dd283874e64386ca0e87dd","datavalue":{"value":{"entity-type":"item","numeric-id":21136,"id":"Q21136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961914$E198C60E-913A-40EA-8263-4E1593FAABE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2ad21f150c621099eebc7c2e673cd9cf43b81a4e","datavalue":{"value":{"entity-type":"item","numeric-id":24376,"id":"Q24376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961914$642EF2DD-6EA3-4268-A71F-1007CED11C3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9301974fbdbf3896f705a4c8ed840f169a9b63f","datavalue":{"value":{"entity-type":"item","numeric-id":19182,"id":"Q19182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961914$5FCCBB24-23B9-4B2C-8D21-7B999016FE4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961914$93D98AA3-75AE-4CF5-AEA2-4815736CDA6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"91328e3ac5dfce9b45d01b607b8d8c272a5b6733","datavalue":{"value":{"entity-type":"item","numeric-id":14670,"id":"Q14670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961914$D8819AD8-7B40-412E-BF45-D30C146928DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961914$2D016D04-07DE-4A70-B915-B4CCBA4C47A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bcecfdfcc6b6cde789a5ef307812b238fed9bee3","datavalue":{"value":{"entity-type":"item","numeric-id":41250,"id":"Q41250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1961914$5DCFFAD6-640B-4002-A9BB-ECC1647AB753","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":"Q1961914$8406F7B0-25AD-4F9D-AC68-EA3BEEF8DC09","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e3cbf3fba196539b146fe77f7a47cddd2e969ad0","datavalue":{"value":"https://doi.org/10.1023/a:1006269330992","type":"string"},"datatype":"url"},"type":"statement","id":"Q1961914$7737C8D1-14E4-4423-9FE6-82585F7ACE64","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b7f68096f56822aa9555e84cecb13fc3ac7c8de2","datavalue":{"value":"W1488122270","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961914$F8765F40-0BD7-40A2-A5EB-63DA2208C1CE","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"2e00db5a89eb14bf4a7d3c3eae6cfc91669bbc67","datavalue":{"value":"Q56092193","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1961914$82ABAE11-D83B-42AD-8380-5E2BC8F43D6D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3f6f8e4fb92c5e9f8415dedf91c1faa12b8ea2a4","datavalue":{"value":{"entity-type":"item","numeric-id":3523168,"id":"Q3523168"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"207445421d5bf377ca3ce3b402c4f6c5a622116d","datavalue":{"value":{"amount":"+0.7389000654220581","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":"Q1961914$E78D754A-72E3-4C97-86AC-EF2ABFFB3968","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6c013473e7b4cccdc138bb31021c66fd5349a7c5","datavalue":{"value":{"entity-type":"item","numeric-id":4944854,"id":"Q4944854"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fa0f1c40fc6db470dbf24d37d5a6b24d4c59733f","datavalue":{"value":{"amount":"+0.7345871925354004","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":"Q1961914$B725C5CD-98A3-4F97-B33E-F0ACD2E2FD5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6d5c10f469ebd8973e02cfaae23e4767153b3bb7","datavalue":{"value":{"entity-type":"item","numeric-id":2723411,"id":"Q2723411"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dc66011a2d7a76a309c7c2b7cd68109914595f75","datavalue":{"value":{"amount":"+0.7344738841056824","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":"Q1961914$8B5E79A7-6697-4178-82E3-4A591CE8E9FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"be6750cd750a678c63f2278474a446b88f4518bb","datavalue":{"value":{"entity-type":"item","numeric-id":5327343,"id":"Q5327343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"75fbb3354aea5f94f36ab641afac8cbbe1427d39","datavalue":{"value":{"amount":"+0.7319498658180237","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":"Q1961914$C6A701BE-EA02-4BDB-8BE3-F74B77BE1538","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5bfbdc296779e4aa3e9eb2bcb8d4501ec95bc6f1","datavalue":{"value":{"entity-type":"item","numeric-id":915498,"id":"Q915498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"88cf64932ae4efdab8f6ee6445f28a5fab1f08bc","datavalue":{"value":{"amount":"+0.7213714122772217","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":"Q1961914$89057A75-BA20-4B0B-8C0E-2238F38CA446","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1961914","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1961914"}}}}}