{"entities":{"Q40322":{"pageid":40378,"ns":120,"title":"Item:Q40322","lastrevid":105427100,"modified":"2026-10-09T10:06:51Z","type":"item","id":"Q40322","labels":{"en":{"language":"en","value":"Algebraic Numbers"}},"descriptions":{"en":{"language":"en","value":"AFP entry Algebraic_Numbers"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"cd29e2c9e738e8fab88394b61c8e6e8203dd7dea","datavalue":{"value":"28608","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40322$1A2A7707-6D16-461D-A7F8-26E8D083505E","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":"Q40322$E7B6B57F-38E9-4934-9EFD-CAFCB0FD1638","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"d373b288da4b8e7ddbdacae5ee09629a38b47d17","datavalue":{"value":"https://www.isa-afp.org/entries/Algebraic_Numbers.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40322$6F331188-CB99-48A9-8DF6-57F4F1A2C2BA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"fd3cd3c8cd085ac2048034c2279872658062342d","datavalue":{"value":"11","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40322$CC5234B9-62DD-4BCD-96BD-35120838BBBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5f5c899803a3ce2dc0dd1263cc65df28aab94054","datavalue":{"value":"12","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40322$55A49244-FE39-47B1-AFF7-F48E334EAD62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8befc1ffe367aef867e4dcd902eb59cbacd3a347","datavalue":{"value":"13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40322$30375F07-85DB-40DE-9AD2-A955DC51485A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40322$FC6F63BE-C8A4-4762-BC98-76276DB56704","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2230d337deb7b90f21aa1a2ec63051e97d36fcd5","datavalue":{"value":"12.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40322$7B2D78FF-6CB9-49D1-AFA0-EBA285749527","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"62b7e192ddad84e0999f497c95811da22d169570","datavalue":{"value":"13.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40322$4904A5E8-92C2-46CF-A2D6-F6DB8F7B8520","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40322$3365D3BD-99F1-4EBD-B339-2C96487A86F2","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":"Q40322$D8DEBE45-4330-4A4C-BC6B-75C59AF1F849","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":"Q40322$C14283CA-B92B-42F0-A55A-F482542B6EEC","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":"Q40322$53EC082A-0D95-4A72-96CC-3593CB89E002","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":"Q40322$F2009862-667F-4DE5-9AF6-2E3A8FBBF20C","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":"Q40322$EECDA95D-63E3-443B-A0E4-13C588EF6211","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":"Q40322$691F8D7E-5CD6-41F2-AF70-703AA5144453","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":"Q40322$3BE54B03-ABF7-4DA7-9536-A60884E0FBDE","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":"Q40322$014AED50-D319-4C94-A1B5-2EEF5D937A2B","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":"Q40322$E7B67E89-02DD-4B97-A9AE-D144B38E0C92","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":"Q40322$4382A9FA-B956-43F2-88E5-6687A3BAB2D6","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":"Q40322$992050D7-96DA-411E-A481-7F95ED883055","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":"Q40322$9DAF9B20-6D39-4F10-869C-E3E263582B42","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":"Q40322$B442584A-23D1-4BB4-955D-DABE37414BEA","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":"Q40322$B93687AB-84D8-47C8-8CE7-FC2CEC5577BC","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":"Q40322$7300E942-6BAA-404F-8039-F2422E734C9A","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":"Q40322$AD239BC5-0366-4EE3-9CA7-2AB4439E9893","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":"Q40322$ACB78005-C48C-48DD-B80F-4039A43A9D53","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":"Q40322$65DB5AEC-D243-4F62-8587-9CE49F0AD197","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":"Q40322$EC6F3650-AEE3-4F86-9114-D7713FA4CF4D","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":"Q40322$D1CBFCBA-B6B5-4C9B-AC31-0389E81EBD31","rank":"normal"}],"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":"Q40322$EF84A68C-231B-4511-A092-261537B0E5EB","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"3e961f1f2b2e533bd88ffdbcd178bd2ef2813f73","datavalue":{"value":"Ren\u00e9 Thiemann","type":"string"},"datatype":"string"},"type":"statement","id":"Q40322$996E14A3-4448-495C-BBD8-9A62B8C2353F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"4e646f16cde9cfa1c19d0771a8f74ba7e8c772f6","datavalue":{"value":"Akihisa Yamada","type":"string"},"datatype":"string"},"type":"statement","id":"Q40322$32984E1C-E952-4F1A-B480-A396F94DE2D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"68caf737a72c94bcb2627452f3944631c5b3bfaa","datavalue":{"value":"Sebastiaan J. C. Joosten","type":"string"},"datatype":"string"},"type":"statement","id":"Q40322$7648CC27-9491-4E6F-A98F-8C15BC19D99C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"85859c7ab42dcb8b36208f2902b7ce0d86423a6f","datavalue":{"value":"Manuel Eberl","type":"string"},"datatype":"string"},"type":"statement","id":"Q40322$2E5149A0-E50B-49D4-8E26-01013138CC9E","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":"Q40322$53881538-2B67-41FC-9780-070D37BE8324","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":"Q40322$488A7B37-22C9-4299-987A-6583170EA3B5","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":"Q40322$9F02A490-9EE9-40F9-969F-7BC6FEDEA6A9","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":"Q40322$A35512EF-74E7-4DF7-830C-9A51E0B60B08","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":"Q40322$AC14A12B-4D00-4333-8716-08877E6EA883","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":"Q40322$E62E819F-1F2A-4627-BAB0-148CD649E3B3","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":"Q40322$DFC33718-FA2C-4DAE-91F2-59D3CAC248B1","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":"Q40322$BDC0E73E-19DD-43F7-B2A7-0F04550AFE15","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":"Q40322$18890626-C876-4795-B61F-1B02F7B1BBD2","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":"Q40322$BD818137-B4BD-44F3-BAE3-34AC3A2824F3","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":"Q40322$52F79C22-58BA-4885-81AA-D09B40060AA5","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":"Q40322$F5D13FF5-FA25-4AD9-B4A1-680D919B56FF","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":"Q40322$36F42EC3-389E-4DF3-B7C8-8C6768718955","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":"Q40322$E5C3C8E8-C69E-4656-80B4-1040DD16CECF","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":"Q40322$2F02AA7F-CD45-4A1D-8423-CF0F2B3DF871","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":"Q40322$76E17169-96F4-4845-9B2C-1E2D9F3FF9D7","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":"Q40322$2ED02E7F-95DC-4441-84EE-4FD2C14D2323","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Algebraic Numbers","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Algebraic_Numbers"}}}}}