{"entities":{"Q7361787":{"pageid":31520900,"ns":120,"title":"Item:Q7361787","lastrevid":105369035,"modified":"2026-10-07T13:37:41Z","type":"item","id":"Q7361787","labels":{"en":{"language":"en","value":"Interpolation Polynomials (in HOL-Algebra)"}},"descriptions":{"en":{"language":"en","value":"AFP entry Interpolation_Polynomials_HOL_Algebra"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"647b5632203ddf974a1a31d12c72668d6ecb5ff0","datavalue":{"value":"https://isa-afp.org/entries/Interpolation_Polynomials_HOL_Algebra.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361787$4E3A3EC8-B0DD-405B-B316-8BF10557A36D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a4f930d0c7e79d89a986a80b5c0bcd11bce82030","datavalue":{"value":{"time":"+2022-01-29T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361787$8E25C43F-51E8-4B0E-9AD2-4EA8F219A856","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"08e34730e8843d863438c2ad5795ad3f0ee72024","datavalue":{"value":"Emin Karayel","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361787$866CE896-05F7-4E42-BE64-93FCAFE46CF0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bbb04d129d23dc3229abb730e55cea716e9edbe2","datavalue":{"value":{"text":"Interpolation Polynomials (in HOL-Algebra)","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361787$5027D5F2-B129-432D-8303-0B72979A340A","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"38a180e6d8d34fb4ef9ab2945854d4aa47980a6a","datavalue":{"value":"A well known result from algebra is that, on any field, there is exactly one polynomial of degree less than n interpolating n points [ 1 , \u00a77]. This entry contains a formalization of the above result, as well as the following generalization in the case of finite fields F : There are |F| m-n polynomials of degree less than m \u2265 n interpolating the same n points, where |F| denotes the size of the domain of the field. To establish the result the entry also includes a formalization of Lagrange interpolation, which might be of independent interest. The formalized results are defined on the algebraic structures from HOL-Algebra, which are distinct from the type-class based structures defined in HOL. Note that there is an existing formalization for polynomial interpolation and, in particular, Lagrange interpolation by Thiemann and Yamada [ 2 ] on the type-class based structures in HOL.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361787$07AFDC5C-4467-4889-8037-6CCEB2505916","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"23cf895df288eaea700f2dca457a8f34ec42828c","datavalue":{"value":{"entity-type":"item","numeric-id":5301801,"id":"Q5301801"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361787$DDDE6303-2F16-477C-9D60-0656AC7A22D6","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":"Q7361787$D6F6CB4D-9DF7-482A-B4E9-921D79091FB9","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":"Q7361787$678C7348-1C55-46B2-A9F6-9C51819ED03E","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":"Q7361787$D4868F19-9B82-4C30-AF8E-5E25E6A2CA44","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Interpolation Polynomials (in HOL-Algebra)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Interpolation_Polynomials_(in_HOL-Algebra)"}}}}}