{"entities":{"Q7361619":{"pageid":31520396,"ns":120,"title":"Item:Q7361619","lastrevid":105423725,"modified":"2026-10-08T13:45:36Z","type":"item","id":"Q7361619","labels":{"en":{"language":"en","value":"Algebraic Numbers in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"AFP entry Algebraic_Numbers"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3d1444e856bbf18681bec548f020da2a855b4667","datavalue":{"value":"https://isa-afp.org/entries/Algebraic_Numbers.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361619$801B0BFB-6130-406D-999E-9D08E9941A27","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"3e961f1f2b2e533bd88ffdbcd178bd2ef2813f73","datavalue":{"value":"Ren\u00e9 Thiemann","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361619$CC08AF76-6B86-436B-8968-18F42BBD64BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"4e646f16cde9cfa1c19d0771a8f74ba7e8c772f6","datavalue":{"value":"Akihisa Yamada","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361619$9B244CC0-99BE-4448-8D25-3B97328822A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"68caf737a72c94bcb2627452f3944631c5b3bfaa","datavalue":{"value":"Sebastiaan J. C. Joosten","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361619$DE6C2A6D-49A8-4FA5-8D5E-9775C9F00758","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"85859c7ab42dcb8b36208f2902b7ce0d86423a6f","datavalue":{"value":"Manuel Eberl","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361619$80F8D746-DC05-4014-85BA-C1B52789CBCE","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"ebf464f02ed29cca7014d9d932e363ddc24e36ab","datavalue":{"value":"Based on existing libraries for matrices, factorization of rational polynomials, and Sturm's theorem, we formalized algebraic numbers in Isabelle/HOL. Our development serves as an implementation for real and complex numbers, and it admits to compute roots and completely factorize real and complex polynomials, provided that all coefficients are rational numbers. Moreover, we provide two implementations to display algebraic numbers, an injective and expensive one, or a faster but approximative version. To this end, we mechanized several results on resultants, which also required us to prove that polynomials over a unique factorization domain form again a unique factorization domain.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361619$013AA9AD-6C66-4C98-882B-DF59D17C5091","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"31385ef3ca1eb53ed08bbfa48b8b91d2510acbaf","datavalue":{"value":{"entity-type":"item","numeric-id":4282674,"id":"Q4282674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$370617C0-0D46-4E4E-A618-9C5F86A4E272","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8ae2d2158e3c465c93233b4442630df5c29733e","datavalue":{"value":{"entity-type":"item","numeric-id":3522019,"id":"Q3522019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$A5BAAF57-D837-4430-B680-0C01A5A417DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f259479a384f8ecfe337d79512b22e03f359c6b3","datavalue":{"value":{"entity-type":"item","numeric-id":5550483,"id":"Q5550483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$73D34792-03D1-4875-9E8E-156AE4E1D193","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0aef60bd392ccfb5e82daa98f095917b33d1745","datavalue":{"value":{"entity-type":"item","numeric-id":3183545,"id":"Q3183545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$E1597B40-1609-483F-808E-6EE5A4023180","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8140e4105e9a133f88717f08d7a9ce19bb1f9cab","datavalue":{"value":{"entity-type":"item","numeric-id":5277869,"id":"Q5277869"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$996C4B6A-1E50-499E-9058-E028652AE1A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"094a19452f4a2cac731a8f91e8d3d9444cc1deea","datavalue":{"value":{"entity-type":"item","numeric-id":1491721,"id":"Q1491721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$2113F7FF-0815-423C-9502-052054EA5DCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b6d0ff209a8c00e6853b2c43b2e31810805788f0","datavalue":{"value":{"entity-type":"item","numeric-id":3935355,"id":"Q3935355"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$2BCDBA04-A5A0-4BB4-9333-C0148E48CC49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d53d3fc5ef0eaf03448b2958c7b38baf170d7b9b","datavalue":{"value":{"entity-type":"item","numeric-id":928655,"id":"Q928655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$0DFB5F00-132F-45EE-A688-2A8917538166","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"73402f4152dc1b0c6384814fa1868f011d7bebc5","datavalue":{"value":{"entity-type":"item","numeric-id":3421016,"id":"Q3421016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$0A2AE3A2-6719-435E-81D3-7211B9713C1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"97132178938a086d46887cf71f3c6653c803319d","datavalue":{"value":{"entity-type":"item","numeric-id":3582701,"id":"Q3582701"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$0D8E2A5E-F64D-44D0-A32C-2CC629B93B58","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"58b378310c3c01d83cef379d83129d9bd06f9769","datavalue":{"value":{"entity-type":"item","numeric-id":7361750,"id":"Q7361750"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$3BC69BE1-00B3-4E0E-80AC-CDA889C00F02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"902a200df68efe27ce065ea2c04682ea087ef202","datavalue":{"value":{"entity-type":"item","numeric-id":7361263,"id":"Q7361263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$9C581A74-C033-4FD8-918E-821DEC0BE4D3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c99d2e3f4402b81f71c762e3f805919871c7a908","datavalue":{"value":{"time":"+2015-12-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361619$CF5E9733-874F-4EDC-A49B-D002BF6A2190","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5757b25e69329be329ad7937908c1a60dd108975","datavalue":{"value":{"text":"Algebraic Numbers in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361619$C2A823DA-85A6-4FCD-BF39-5B8E2D186C9A","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$EC94C991-2120-42B1-93D1-4BC8EA63FF09","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"65292b3c42fa1bd5c21e4c91fe94fdc3f630f232","datavalue":{"value":{"entity-type":"item","numeric-id":7360821,"id":"Q7360821"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$A073751B-DEEA-4A5D-BBEC-D3C907196851","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$9B01B46B-2234-4037-ABC2-66EF04DA703C","rank":"normal"}],"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"cd29e2c9e738e8fab88394b61c8e6e8203dd7dea","datavalue":{"value":"28608","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361619$A20AF2BF-1281-4026-BD97-FB6466BBDBD1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"fd3cd3c8cd085ac2048034c2279872658062342d","datavalue":{"value":"11","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361619$722DEC8F-833F-4D08-BF9C-1768743A3A26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2230d337deb7b90f21aa1a2ec63051e97d36fcd5","datavalue":{"value":"12.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361619$177FD086-E6F9-4B16-B0A1-890B3CA24053","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"62b7e192ddad84e0999f497c95811da22d169570","datavalue":{"value":"13.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361619$F52E3263-3807-4F87-BBBD-85DE6DCE4032","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361619$B0DD3D5D-3725-4DB6-AAC4-B61BB16FBDC0","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$9B33602A-E675-4820-9AD7-5112F64AAA54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cea2a7e9bb130921d12e1d361b3d4585036772c9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$65B02417-E8A8-478D-A8DE-30BCC7DA5A78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$26CAB33D-5372-4DE1-BFCD-D193407F0569","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$EBEF94EC-CCCF-4EE0-A065-74A1B4C3635E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8d55daeff7c4288ce44d22059c68add0e43c0b42","datavalue":{"value":{"entity-type":"item","numeric-id":40280,"id":"Q40280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$EB233D51-40F4-4D7A-9314-A1A2D79ADF3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"47f96c29829067516c9fd587e32502374da65084","datavalue":{"value":{"entity-type":"item","numeric-id":43910,"id":"Q43910"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$86F1AEA2-EBD6-4B73-AD58-F7E828AC45C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9f7773444cba07bf64d0a42509b5f6e8b2964659","datavalue":{"value":{"entity-type":"item","numeric-id":43939,"id":"Q43939"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$C896C51A-06FF-45FF-884B-73180132197A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$8E78476F-C692-4A6C-8A9D-B6F90D6B3BD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc4eff68b160f30b8d66dfcb610a0ea7a927079b","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$79497D82-FD6A-4C8F-A395-8C9060BA9935","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"24c387ececd24fa7a9a4716819d51e1718cd572b","datavalue":{"value":{"entity-type":"item","numeric-id":13328,"id":"Q13328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$B29D3E2A-FC52-4B74-BD25-6A26676E0F5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"03281999c3208b8f3a62eaceadadf1ce834fe219","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$7D950929-4345-4906-B651-A86CD46EAF76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"e24c7515283a4e060be51f07ba9d059646ad882b","datavalue":{"value":{"entity-type":"item","numeric-id":43927,"id":"Q43927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$85672BEA-B4C9-4AF3-9C10-12ABEE8DF3BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"331995fe532c23e24d72d01a1bd6245fafcd9671","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$AF839637-CCB6-4EB5-8325-40877E1DC5A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"654080dee7524f5000d195afeb10c1de4245a272","datavalue":{"value":{"entity-type":"item","numeric-id":13503,"id":"Q13503"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$81C74CAC-1A2C-40E8-868D-0107176F5448","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9eb436930ab1f6d235b354c651322b547341064b","datavalue":{"value":{"entity-type":"item","numeric-id":13309,"id":"Q13309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$E34FBE16-D2C4-497F-8DEF-249B2A6AD6A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"053ea061eb2db1c9b7f27b25da993bb19055407c","datavalue":{"value":{"entity-type":"item","numeric-id":25224,"id":"Q25224"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$26D0E53D-A729-48BC-8BBF-AD5503E7C69C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8d0e581a152a84598efe5a4e592ec4113e00b9c7","datavalue":{"value":{"entity-type":"item","numeric-id":13434,"id":"Q13434"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$5055146F-BCA2-46BB-A445-0995C3F4E71B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"206148fb4091bc526b4985eb7106f34e5f9739ba","datavalue":{"value":{"entity-type":"item","numeric-id":52541,"id":"Q52541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$F93468AA-0BF8-437B-89E9-0EA8D0A36E92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"19c595020292c8ce475b0c10b4d6d2a5bb12aab8","datavalue":{"value":{"entity-type":"item","numeric-id":13238,"id":"Q13238"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$9E5679AC-2015-4722-8CB7-8C5750DCFA28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"4c898c87389aba87e0bd281dea252635e56d3c7a","datavalue":{"value":{"entity-type":"item","numeric-id":5973395,"id":"Q5973395"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361619$A9D72BBE-6DDA-4700-8180-9A3B40A12428","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Algebraic Numbers in Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Algebraic_Numbers_in_Isabelle/HOL"}}}}}