{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,23]],"date-time":"2024-09-23T12:40:12Z","timestamp":1727095212350},"reference-count":9,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T00:00:00Z","timestamp":1693526400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/3.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,9,1]]},"abstract":"Summary<\/jats:title>\n The article concerns about formalizing multivariable formal power series and polynomials [3] in one variable in terms of \u201cbag\u201d (as described in detail in [9]), the same notion as multiset over a finite set, in the Mizar system [1], [2]. Polynomial rings and ring of formal power series, both in one variable, have been formalized in [6], [5] respectively, and elements of these rings are represented by infinite sequences of scalars. On the other hand, formalization of a multivariate polynomial requires extra techniques of using \u201cbag\u201d to represent monomials of variables, and polynomials are formalized as a function from bags of variables to the scalar ring. This means the way of construction of the rings are different between single variable and multi variables case (which implies some tedious constructions, e.g. in the case of ten variables in [8], or generally in the problem of prime representing polynomial [7]). Introducing bag-based construction to one variable polynomial ring provides straight way to apply mathematical induction to polynomial rings with respect to the number of variables. Another consequence from the article, a polynomial ring is a subring of an algebra [4] over the same scalar ring, namely a corresponding formal power series. A sketch of actual formalization of the article is consists of the following four steps:<\/jats:p>\n 1. translation between Bags 1<\/jats:bold> (the set of all bags of a singleton) and N;<\/jats:p>\n 2. formalization of a bag-based formal power series in multivariable case over a commutative ring denoted by Formal-Series<\/jats:bold>(n, R<\/jats:italic>);<\/jats:p>\n 3. formalization of a polynomial ring in one variable by restricting one variable case denoted by Polynom-Ring<\/jats:bold>(1, R<\/jats:italic>). A formal proof of the fact that polynomial rings are a subring of Formal-Series<\/jats:bold>(n, R<\/jats:italic>), that is R<\/jats:italic>-Algebra, is included as well;<\/jats:p>\n 4. formalization of a ring isomorphism to the existing polynomial ring in one variable given by sequence: Polynom-Ring<\/jats:bold>(1, R<\/jats:italic>) \u2192\u02dc Polynom-Ring<\/jats:bold>\n.<\/jats:p>","DOI":"10.2478\/forma-2023-0001","type":"journal-article","created":{"date-parts":[[2023,9,27]],"date-time":"2023-09-27T06:29:45Z","timestamp":1695796185000},"page":"1-8","source":"Crossref","is-referenced-by-count":0,"title":["On Bag of 1. Part I"],"prefix":"10.2478","volume":"31","author":[{"given":"Yasushige","family":"Watase","sequence":"first","affiliation":[{"name":"Suginami-ku Matsunoki 6, 3-21 Tokyo Japan"}]}],"member":"374","published-online":{"date-parts":[[2023,9,26]]},"reference":[{"key":"2024092312053370381_j_forma-2023-0001_ref_001","doi-asserted-by":"crossref","unstructured":"Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, Karol P\u0105k, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261\u2013279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007\/978-3-319-20615-8 17.","DOI":"10.1007\/978-3-319-20615-8_17"},{"key":"2024092312053370381_j_forma-2023-0001_ref_002","doi-asserted-by":"crossref","unstructured":"Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, and Karol P\u0105k. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9\u201332, 2018. doi:10.1007\/s10817-017-9440-6.","DOI":"10.1007\/s10817-017-9440-6"},{"key":"2024092312053370381_j_forma-2023-0001_ref_003","unstructured":"Edward J. Barbeau. Polynomials. Springer, 2003."},{"key":"2024092312053370381_j_forma-2023-0001_ref_004","doi-asserted-by":"crossref","unstructured":"Adam Grabowski, Artur Korni\u0142owicz, and Christoph Schwarzweller. On algebraic hierarchies in mathematical repository of Mizar. In M. Ganzha, L. Maciaszek, and M. Paprzycki, editors, Proceedings of the 2016 Federated Conference on Computer Science and Information Systems (FedCSIS), volume 8 of Annals of Computer Science and Information Systems, pages 363\u2013371, 2016. doi:10.15439\/2016F520.","DOI":"10.15439\/2016F520"},{"key":"2024092312053370381_j_forma-2023-0001_ref_005","unstructured":"Ewa Gr\u0105dzka. The algebra of polynomials. Formalized Mathematics, 9(3):637\u2013643, 2001."},{"key":"2024092312053370381_j_forma-2023-0001_ref_006","unstructured":"Robert Milewski. The ring of polynomials. Formalized Mathematics, 9(2):339\u2013346, 2001."},{"key":"2024092312053370381_j_forma-2023-0001_ref_007","doi-asserted-by":"crossref","unstructured":"Karol P\u0105k. Prime representing polynomial. Formalized Mathematics, 29(4):221\u2013228, 2021. doi:10.2478\/forma-2021-0020.","DOI":"10.2478\/forma-2021-0020"},{"key":"2024092312053370381_j_forma-2023-0001_ref_008","doi-asserted-by":"crossref","unstructured":"Karol P\u0105k. Prime representing polynomial with 10 unknowns. Formalized Mathematics, 30(4):255\u2013279, 2022. doi:10.2478\/forma-2022-0021.","DOI":"10.2478\/forma-2022-0021"},{"key":"2024092312053370381_j_forma-2023-0001_ref_009","doi-asserted-by":"crossref","unstructured":"Piotr Rudnicki, Christoph Schwarzweller, and Andrzej Trybulec. Commutative algebra in the Mizar system. Journal of Symbolic Computation, 32(1\/2):143\u2013169, 2001. doi:10.1006\/jsco.2001.0456.","DOI":"10.1006\/jsco.2001.0456"}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.sciendo.com\/pdf\/10.2478\/forma-2023-0001","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,23]],"date-time":"2024-09-23T12:05:42Z","timestamp":1727093142000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.2478\/forma-2023-0001"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,1]]},"references-count":9,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2023,9,26]]},"published-print":{"date-parts":[[2023,9,1]]}},"alternative-id":["10.2478\/forma-2023-0001"],"URL":"http:\/\/dx.doi.org\/10.2478\/forma-2023-0001","relation":{},"ISSN":["1898-9934"],"issn-type":[{"type":"electronic","value":"1898-9934"}],"subject":[],"published":{"date-parts":[[2023,9,1]]}}}