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

<p>The article concerns about formalizing a certain lemma on embedding of algebraic structures in the Mizar system, claiming that if a ring <italic>A</italic> is embedded in a ring <italic>B</italic> then there exists a ring <italic>C</italic> which is isomorphic to <italic>B</italic> and includes <italic>A</italic> as a subring. This construction applies to algebraic structures such as Abelian groups and rings.</p>
</abstract>

The article concerns about formalizing a certain lemma on embedding of algebraic structures in the Mizar system, claiming that if a ring A is embedded in a ring B then there exists a ring C which is isomorphic to B and includes A as a subring. This construction applies to algebraic structures such as Abelian groups and rings.

Embedding Principle for Rings and Abelian Groups

Formalized Mathematics

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

{"article-title":"Embedding Principle for Rings and Abelian Groups"}

The article concerns about formalizing a certain lemma on embedding of algebraic structures in the Mizar system, claiming that if a ring A is embedded in a...

Embedding Principle for Rings and Abelian Groups

Published Online: Dec 23, 2023

Page range: 143 - 150

Accepted: Nov 21, 2023

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

Keywords
Abelian group, ring, embedding

© 2023 Yasushige Watase, published by Sciendo

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

Embedding Principle for Rings and Abelian Groups

Published Online: Dec 23, 2023

Page range: 143 - 150

Accepted: Nov 21, 2023

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

KeywordsAbelian group, ring, embedding

© 2023 Yasushige Watase, published by Sciendo

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

Keywords
Abelian group, ring, embedding