{"entities":{"Q5739892":{"pageid":7769444,"ns":120,"title":"Item:Q5739892","lastrevid":58607055,"modified":"2026-04-05T23:38:09Z","type":"item","id":"Q5739892","labels":{"en":{"language":"en","value":"Formalized linear algebra over elementary divisor rings in \\textsc{Coq}"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6601110"}},"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":"Q5739892$F861FA00-9620-4454-BCE8-3226D392211C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9ec7725515fd962e6e717dfc93e72bc80859de2c","datavalue":{"value":{"text":"Formalized linear algebra over Elementary Divisor Rings in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5739892$B8A62A09-F768-4F10-BE59-D103E95D30B0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c45a434dfea5ed40d5509c6c9f4048d4d9f31151","datavalue":{"value":"1448.68461","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5739892$A9B92AF8-BE3C-4ED0-8877-1E697557BE1F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"616bcf9c634feecf5ce2847cea92780a38357739","datavalue":{"value":"10.2168/LMCS-12(2:7)2016","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5739892$1F55FFD2-766D-4DD9-90ED-FBA69ED1BE77","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1c340bbe3cb06f9d0bd2877b035f7ed1faf56b41","datavalue":{"value":{"entity-type":"item","numeric-id":5739891,"id":"Q5739891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5739892$9E2AA89E-0EAB-4F7F-B730-EA2694A69343","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"110c9b9e0e852b5bffe2fcd42275bf67a9f49ee7","datavalue":{"value":{"entity-type":"item","numeric-id":375195,"id":"Q375195"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5739892$9F28AD4F-080E-4F7F-8D55-0750F49CDF05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"343748d25c380d16ff7d424df96b35bd8fa80111","datavalue":{"value":{"entity-type":"item","numeric-id":2900559,"id":"Q2900559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5739892$1405EF2C-58A6-470A-84A5-418BCC1F4F50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"37b6655ff0c1854542b6f28c9af39f0877a44635","datavalue":{"value":{"entity-type":"item","numeric-id":2319989,"id":"Q2319989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5739892$C5F95DF7-58A0-44B8-944C-7F1E8C587CEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9837115d701db3c6d1129817eee769862467ad1e","datavalue":{"value":{"entity-type":"item","numeric-id":2844695,"id":"Q2844695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5739892$4996ECBC-8168-4A9D-AE04-ED43622D3F81","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"da58c52dc46c86e7440f2499c9e1bef3537c5562","datavalue":{"value":{"entity-type":"item","numeric-id":2786118,"id":"Q2786118"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5739892$830FE569-2F8A-4F80-BC2D-3D49D07AD347","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"aa0c76dadf16d518dc4d05a67d37c73c921d6123","datavalue":{"value":{"time":"+2016-07-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5739892$A7FB164A-6A4C-4CF4-B65E-993C75C51D75","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7109410064bf4ca7035ae1d4a449893558759ce6","datavalue":{"value":"https://arxiv.org/abs/1601.07472","type":"string"},"datatype":"url"},"type":"statement","id":"Q5739892$CDD28EC4-B126-4E41-8801-7E633CFE7E9D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5739892$3FC64EBC-F842-4735-8A4F-24895F897E55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"bbe2dde55566c57c31463992aac9b72d0f8c104e","datavalue":{"value":"15B33","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5739892$1400B128-0138-4E55-A99F-3E660EAC10D8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ef0e83c3dbb0e407598dc8b1819e42662122564c","datavalue":{"value":"6601110","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5739892$271E00BE-CA82-401A-914F-DB67E5FAD8D5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"658126897c7f6bf3db78fea48b2876524c1d8c9e","datavalue":{"value":"formalization of mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q5739892$16C9CBE0-3143-4E1E-BFF6-B340D3986396","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f05b96a3b56bcbf16250553557f268d9b9e694ce","datavalue":{"value":"constructive algebra","type":"string"},"datatype":"string"},"type":"statement","id":"Q5739892$4CECDFD1-F745-48CC-AF12-A57B68B05086","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q5739892$4B27A561-8265-4496-B24B-7CEE9328929E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ac0fdcef04bd18fdb2c1db8188d6e228ee53b085","datavalue":{"value":"Ssreflect","type":"string"},"datatype":"string"},"type":"statement","id":"Q5739892$74F4E02D-23AC-4541-B98D-B09D8CEE80C7","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c652637493e8de65377ba80065ca4183c6dc627","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5739892$AE13B2A0-D1BF-4F5D-A311-5FC8D414927B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ef03848f41f59da431665c121436ac0a6bc94ac2","datavalue":{"value":{"entity-type":"item","numeric-id":13610,"id":"Q13610"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5739892$ECE5C8BC-6137-45A8-8FC8-2A84DCCD3F55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"517f90dc7229d7e4bd6931fbbf5d99cb4c838f37","datavalue":{"value":{"entity-type":"item","numeric-id":13171,"id":"Q13171"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5739892$4FC2CCA1-E284-43F6-BE6A-450A41A3C599","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9337f62f2e2e1a0506e5668f45d3e954d0bc5d5","datavalue":{"value":{"entity-type":"item","numeric-id":16057,"id":"Q16057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5739892$2E0A3118-1CCA-4560-BF4B-6B8C9EEF422D","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":"Q5739892$0E1FA6AD-4FA0-47FA-9908-97A947C540A6","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":"Q5739892$AC9ACDDA-7649-444A-8976-0AF48AF8F81B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5739892$B937D216-B7EA-4CB1-A657-E0BFFB539852","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":"Q5739892$C8DA79A5-3B02-4993-A857-6585273DF009","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c2f988d4bf8ade6d6b757e30abe9b70bc5c61113","datavalue":{"value":"W3104555329","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5739892$6D588B3E-F285-4343-BAFD-0F506E5E6F18","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d8c9e0eec8bc42f69526d09ccf47a9e2b281f0c2","datavalue":{"value":{"entity-type":"item","numeric-id":4916066,"id":"Q4916066"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1e96205cd814c0043b9eb3e441f361a37a96c891","datavalue":{"value":{"amount":"+0.7896210551261902","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":"Q5739892$34B8E7FF-CDE7-45B5-949B-6EF93ACA4474","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0594f4c979126902584456435d87ef9adbc73610","datavalue":{"value":{"entity-type":"item","numeric-id":2102950,"id":"Q2102950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"438f1ef2661885b7498a66017e7315f0dc21e9f1","datavalue":{"value":{"amount":"+0.779666543006897","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":"Q5739892$1F7E6CBB-76A3-414C-B5FE-ADE230941413","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"94e05246b07b174c8fcb0d8a8a08ef10b9e83113","datavalue":{"value":{"entity-type":"item","numeric-id":6108811,"id":"Q6108811"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f1328f832280efde25734049f1b49cc1eadb47ea","datavalue":{"value":{"amount":"+0.7634438276290894","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":"Q5739892$D8A3AAF7-BF89-4A5A-991F-03B45FD8A6E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"73dfdf0763c6e16eb95074b0b07b09ba079119df","datavalue":{"value":{"entity-type":"item","numeric-id":677923,"id":"Q677923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"94df14f95285e4e2a9870db4c2ae03cc7e689898","datavalue":{"value":{"amount":"+0.7594723701477051","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":"Q5739892$8975E84B-A08D-4747-B952-0E7FC6C88A31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9b1fdd9520e602dfc771c2278c107adc0bccaec9","datavalue":{"value":{"entity-type":"item","numeric-id":333325,"id":"Q333325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"088673fd59f77d8aea71f77751df8bcd6f6cf61d","datavalue":{"value":{"amount":"+0.7413645386695862","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":"Q5739892$C27C5C17-79CE-4AC7-81AD-4412CBF0F476","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5739892","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5739892"}}}}}