<abstract xmlns="http://www.w3.org/1999/xhtml">

The article concerns about formalizing multivariable formal power series and polynomials [<xref ref-type="bibr" rid="j_forma-2023-0001_ref_003">3</xref>] in one variable in terms of “bag” (as described in detail in [<xref ref-type="bibr" rid="j_forma-2023-0001_ref_009">9</xref>]), the same notion as multiset over a finite set, in the Mizar system [<xref ref-type="bibr" rid="j_forma-2023-0001_ref_001">1</xref>], [<xref ref-type="bibr" rid="j_forma-2023-0001_ref_002">2</xref>]. Polynomial rings and ring of formal power series, both in one variable, have been formalized in [<xref ref-type="bibr" rid="j_forma-2023-0001_ref_006">6</xref>], [<xref ref-type="bibr" rid="j_forma-2023-0001_ref_005">5</xref>] 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 “bag” 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 [<xref ref-type="bibr" rid="j_forma-2023-0001_ref_008">8</xref>], or generally in the problem of prime representing polynomial [<xref ref-type="bibr" rid="j_forma-2023-0001_ref_007">7</xref>]). 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 [<xref ref-type="bibr" rid="j_forma-2023-0001_ref_004">4</xref>] 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:
1. translation between <bold>Bags 1</bold> (the set of all bags of a singleton) and N;
2. formalization of a bag-based formal power series in multivariable case over a commutative ring denoted by <bold>Formal-Series</bold>(<italic>n, R</italic>);
3. formalization of a polynomial ring in one variable by restricting one variable case denoted by <bold>Polynom-Ring</bold>(1, <italic>R</italic>). A formal proof of the fact that polynomial rings are a subring of <bold>Formal-Series</bold>(<italic>n, R</italic>), that is <italic>R</italic>-Algebra, is included as well;
4. formalization of a ring isomorphism to the existing polynomial ring in one variable given by sequence: <bold>Polynom-Ring</bold>(1, <italic>R</italic>) →˜ <bold>Polynom-Ring</bold>
.
</abstract>

The article concerns about formalizing multivariable formal power series and polynomials [3] in one variable in terms of “bag” (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 “bag” 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:
1. translation between Bags 1 (the set of all bags of a singleton) and N;
2. formalization of a bag-based formal power series in multivariable case over a commutative ring denoted by Formal-Series(n, R);
3. formalization of a polynomial ring in one variable by restricting one variable case denoted by Polynom-Ring(1, R). A formal proof of the fact that polynomial rings are a subring of Formal-Series(n, R), that is R-Algebra, is included as well;
4. formalization of a ring isomorphism to the existing polynomial ring in one variable given by sequence: Polynom-Ring(1, R) →˜ Polynom-Ring
.

On Bag of 1. Part I

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 Public License.

{"article-title":"On Bag of 1. Part I"}

The article concerns about formalizing multivariable formal power series and polynomials [3] in one variable in terms of “bag” (as described in detail in [9]),...

On Bag of 1. Part I

Online veröffentlicht: 26. Sept. 2023

Seitenbereich: 1 - 8

Akzeptiert: 31. März 2023

DOI: https://doi.org/10.2478/forma-2023-0001

Schlüsselwörter
bag, formal power series, polynomial ring

© 2023 Yasushige Watase, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 Public License.

On Bag of 1. Part I

Online veröffentlicht: 26. Sept. 2023

Seitenbereich: 1 - 8

Akzeptiert: 31. März 2023

DOI: https://doi.org/10.2478/forma-2023-0001

Schlüsselwörterbag, formal power series, polynomial ring

© 2023 Yasushige Watase, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 Public License.

Schlüsselwörter
bag, formal power series, polynomial ring