{"entities":{"Q5891671":{"pageid":7927466,"ns":120,"title":"Item:Q5891671","lastrevid":97484339,"modified":"2026-06-05T14:52:40Z","type":"item","id":"Q5891671","labels":{"en":{"language":"en","value":"Formal power series"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6062054"}},"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":"Q5891671$3C04C0E7-4477-4DF1-B68E-F75156EF5EB3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a918ce03ee8b49f485a0c5f42727a45714f05b20","datavalue":{"value":{"text":"Formal power series","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5891671$B09E4AED-A5D9-4CC7-99B7-F2A2BC9A3649","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8320bc28c599b400eb40b52e580878fd47723013","datavalue":{"value":"1266.03022","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5891671$3918DAE6-8D50-40AB-819D-6D0472B49449","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8c973ae8cb97c26cea9e67d82e7a35f420626e2a","datavalue":{"value":{"entity-type":"item","numeric-id":438551,"id":"Q438551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5891671$7DE3E6AD-C24A-4AB4-BD53-786DD12D0FA7","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":"Q5891671$9BDC6065-E003-4522-8603-E35A7846236C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6c7ad691786690cf86127845d28cf47311748286","datavalue":{"value":{"time":"+2012-07-31T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5891671$3062D867-741B-453B-9F50-EFDD159B3A99","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"4440187760bcc7571d62468980c898d2e13443b9","datavalue":{"value":"This paper presents a formalization of the topological ring of formal power series in \\texttt{Isabelle/HOL}.  The following constructions are formalized: division, the formal derivative, various basic manipulations on formal power series (shifting, differentiating, general convolutions and powers), as well as radicals, composition and reverses.  As an example, the exponential, binomial and hyper-geometric series are introduced as characterizing all the solutions of a certain formal differential equation. It is shown that this approach yields extremely short proofs for the binomial theorem and Vandermonde's identity. Also, logarithmic and some trigonometric series are defined; it is shown that some of the properties hold without any convergence consideration. Finally, it is shown that, using a generic formalization of the fraction field of an integral domain, Laurent series and rational functions can be obtained for free.","type":"string"},"datatype":"string"},"type":"statement","id":"Q5891671$3DD6D978-1035-4850-9D8E-252BC31A7910","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"895d5fc798d777f77a43df1e1b11857e28584cdd","datavalue":{"value":{"entity-type":"item","numeric-id":592080,"id":"Q592080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5891671$4C7E9DE2-BF47-43BA-9CBE-D190A1D10F48","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5891671$13B28B66-D538-4A7B-8C83-FD0EB8D6697A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2a32617a282a11119ab5747f7438838c721f0933","datavalue":{"value":"32A05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5891671$03D99F64-775A-432B-B7B5-D12715C584CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5891671$4919ED56-7BC9-468C-A05A-FE18292729D0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e3730cbc05301e9a28920b92a08ff859cb67b0ee","datavalue":{"value":"6062054","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5891671$2FD62CD6-7A72-4AFD-AACD-0C0E9E2F8B49","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"658126897c7f6bf3db78fea48b2876524c1d8c9e","datavalue":{"value":"formalization of mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q5891671$555568E7-5EE2-4363-A2A8-8D51243D5646","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5891671$CA0B9C5E-D09A-4DB1-9996-2EBD0E10A161","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f3590eb8b47f26c41d61639b5166afe44752133e","datavalue":{"value":"formal power series","type":"string"},"datatype":"string"},"type":"statement","id":"Q5891671$2D31C715-0E6E-4137-A409-6DE744AA99BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"931fc00879af8b0f86011ef32c390fa4802ca84e","datavalue":{"value":"generating functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q5891671$D7758627-82A2-43D7-93D6-4DBAB1BA2447","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ca5830b9e054ca240b1ee150695772e6c0bd6aa7","datavalue":{"value":"\\texttt{Isabelle/HOL}","type":"string"},"datatype":"string"},"type":"statement","id":"Q5891671$866EA140-D969-4BA0-A244-AA06C68707FB","rank":"normal"}],"P1463":[{"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":"Q5891671$75A687B6-D39F-41A1-9087-D120732DC698","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5891671$90C99BAA-5BCB-47A4-86DF-F70CE7BDA32F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5891671$FEBA63C0-3734-434D-A028-8E48602113F7","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":"Q5891671$4006D396-4FD5-42BD-B659-8132D11C1376","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a2c2be4284d276b19ac0f980f97f3358c09fbc11","datavalue":{"value":"https://doi.org/10.1007/s10817-010-9195-9","type":"string"},"datatype":"url"},"type":"statement","id":"Q5891671$78CFBD5D-EE03-4D04-B7B6-61B0602585C8","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0e906107a7561f63f84eb19a5afdc4f72b81b8a3","datavalue":{"value":"W2084636036","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5891671$CC2484AE-E7F0-4B5C-8213-8FF25AE99CF7","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d755a13c46d237ac0e0ca8d1b3f0bdb700a0f74","datavalue":{"value":{"entity-type":"item","numeric-id":5505503,"id":"Q5505503"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5891671$ABF5A5FC-B41A-4647-8A46-F2D602340DCB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"54eee2313932f532ca016c516cb047dfc95351e0","datavalue":{"value":{"entity-type":"item","numeric-id":5428257,"id":"Q5428257"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5891671$54B494D4-4238-45EB-BCD2-BE468956ECEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd78fd7539746ce39fface229dfdce943e7717ba","datavalue":{"value":{"entity-type":"item","numeric-id":4320535,"id":"Q4320535"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5891671$766CE90B-74D6-43D6-8A2E-C8CF19726A42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14533123e0b9e73c06f9737a070ee002c25f5f1b","datavalue":{"value":{"entity-type":"item","numeric-id":3612442,"id":"Q3612442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5891671$58652CD9-9949-41AD-BEBD-20C0EC27FED0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b7902ad05fc58101eeb009f9da7bcfeb90392bef","datavalue":{"value":{"entity-type":"item","numeric-id":3608762,"id":"Q3608762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5891671$3428499A-2E75-4607-B5EF-AB8200FFDEEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc0934b5a5fbbee6540a96342864688602c12023","datavalue":{"value":{"entity-type":"item","numeric-id":4039888,"id":"Q4039888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5891671$D7728A88-9095-47AD-8F83-297CB8C24E98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d78f9e51b63c4e692cfd1c2dfcec05b263377e7f","datavalue":{"value":{"entity-type":"item","numeric-id":5477669,"id":"Q5477669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5891671$463C4579-5836-4B85-9F8D-124B00965FC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5891671$8531A682-0D5E-4EF0-8C9B-3D35285D5F71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f4a38cfed3a9dda1b51eba005e5c6949690ed92","datavalue":{"value":{"entity-type":"item","numeric-id":5576282,"id":"Q5576282"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5891671$E1CF2BE4-FA67-4ECB-AF7B-FBC2A96FE0F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c18eae0d93c62338c42d5358a66e2303bf3601de","datavalue":{"value":{"entity-type":"item","numeric-id":1961913,"id":"Q1961913"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5891671$FE8050EF-1457-407B-BAE9-F38240A1258C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce553c7842f1b63d231c944f4632d98f29fafb26","datavalue":{"value":{"entity-type":"item","numeric-id":3995745,"id":"Q3995745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5891671$344FF330-5371-416D-AC6D-6EBE2666C7DE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c461cade1aedd27d5ddfd48f1656a9938a318de2","datavalue":{"value":"10.1007/S10817-010-9195-9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5891671$D4F36A2C-D47B-497A-B68C-2A20759CCCE1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bc0be8e77fe682ba6a690bb873dc1e338648eca6","datavalue":{"value":{"entity-type":"item","numeric-id":2751549,"id":"Q2751549"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6fc1369f92d7d63b662d95db9b21a8f8120b0780","datavalue":{"value":{"amount":"+0.7739402055740356","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":"Q5891671$55F5CD12-2C1A-4278-B3A3-AEA6A09F01CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"36f0ae0b2b4585263b1797b6ba3888079bbf3a61","datavalue":{"value":{"entity-type":"item","numeric-id":2031838,"id":"Q2031838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e9a2a01795e0fe61415eb1eef0b5196f98d3fc6a","datavalue":{"value":{"amount":"+0.7696372270584106","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":"Q5891671$653000E7-717D-403F-99DC-C1C674B9F0FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"34f8e6e10105f8f84ab40abff06724da2b59f5bf","datavalue":{"value":{"entity-type":"item","numeric-id":6133180,"id":"Q6133180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f1a67499a64c4af7ba30092b287f8c5419a225d4","datavalue":{"value":{"amount":"+0.7675458192825317","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":"Q5891671$DA851CD2-8AFE-4290-B580-EDF2E8A360D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"447a338a545d3fe24921b1062a2ef15ce5cfb095","datavalue":{"value":{"entity-type":"item","numeric-id":2392908,"id":"Q2392908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b0832cfcf1c1f81391d5df00b6f9162312cbd19e","datavalue":{"value":{"amount":"+0.766849160194397","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":"Q5891671$C504EE4B-D664-46EB-81DB-D852ABDFF62B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fb17600a1b498b50a1708f98564253b35515fa3f","datavalue":{"value":{"entity-type":"item","numeric-id":5916404,"id":"Q5916404"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3f090d83729f63f98ba652bb28309d5c71f52b75","datavalue":{"value":{"amount":"+0.7601003646850586","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":"Q5891671$9018166A-C271-4749-9E4B-E3812E414BB2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formal power series (scientific article; zbMATH DE number 6062054)","badges":[]}}}}}