@MISC{POLYALGX.MIZ,
  AUTHOR = {Watase, Yasushige},
  TITLE = {{O}n {B}ag of 1. {P}art {I}},
  SECTION1 = {Natural Number vs. Bag of Singleton},
  SECTION2 = {Construct R-Algebra of Multivariate Formal Power Series},
  SECTION3 = {Construct Isomorphism from Formal-Series(1,R) to Formal-Series R},
  SECTION4 = {Construct Isomorphism from Polynom-Ring(1,R) to Polynom-Ring R},
  DAY = {31},
  MONTH = {March},
  YEAR = {2023},
  ADDRESS1 = {Suginami-ku Matsunoki 6, 3-21 Tokyo\\Japan},
  SUMMARY = {The article concerns about formalizing multivariable formal power series and  
  polynomials in one variable in terms of ``bag", the same notion as multiset over a finite set, 
  in the Mizar System   \cite{Mizar-State-2015}. 
  Polynomial rings and ring of formal power series, both in one variable have formalized in   
  \cite{POLYNOM3.ABS,POLYALG1.ABS} 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. 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   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:
  \begin{enumerate} 
  \item translation between $\mathrm{\textbf{Bags 1}}$(the set of all bags of a singleton) 
  and $  \mathrm{\mathbb{N}},$ 
  \item formalize a bag-based formal power series in multivariable over a 
  commutative ring denoted by $\mathrm{\textbf{Formal-Series}(n,R)}$,
  \item formalize a polynomial ring in one variable by restricting formalize a 
  formal power series in one variable denoted by $\mathrm{\textbf{Polynom-Ring}(1,R)}.$ 
  \\A formal proof of the polynomial rings are a sub-ring of $\mathrm{\textbf{Formal-Series}(n,R)}$ that 
  is $\mathrm  {R}$-Algebra is included as well,
  \item formalize a ring isomorphism to the existing polynomial ring in one variable constructed  
  by sequence:
  $\mathrm{\textbf{Polynom-Ring}(1,R)} \stackrel{\sim}{\longrightarrow} \mathrm{\textbf{Polynom-  Ring} \ R}$. 
  \end{enumerate}},
  MSC2010 = {13F25 13B25 03B35},
  KEYWORDS = {Bag; Formal Power Series; Polynomial Ring}}

@BOOK{Zariski1975,
 AUTHOR={Zariski, Oscar and Samuel, Pierre},
 TITLE={Commutative Algebra {I}},
 edition={2nd},
 publisher={Springer},
 year={1975}}
 
@BOOK{Shafarevich2003,
 AUTHOR={Igor R. Shafarevich},
 TITLE={Discourses on Algebra},
 PUBLISHER={Springer Berlin, Heidelberg},
 YEAR=2003,
 ISBN = {978-3-540-42253-2}}
} 
