<abstract xmlns="http://www.w3.org/1999/xhtml"><p> In this article, conservation rules of the direct sum decomposition of groups are mainly discussed. In the first section, we prepare miscellaneous definitions and theorems for further formalization in Mizar [5]. In the next three sections, we formalized the fact that the property of direct sum decomposition is preserved against the substitutions of the subscript set, flattening of direct sum, and layering of direct sum, respectively. We referred to [14], [13] [6] and [11] in the formalization.</p></abstract>

In this article, conservation rules of the direct sum decomposition of groups are mainly discussed. In the first section, we prepare miscellaneous definitions and theorems for further formalization in Mizar [5]. In the next three sections, we formalized the fact that the property of direct sum decomposition is preserved against the substitutions of the subscript set, flattening of direct sum, and layering of direct sum, respectively. We referred to [14], [13] [6] and [11] in the formalization.

Conservation Rules of Direct Sum Decomposition of Groups

Formalized Mathematics

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

{"article-title":"Conservation Rules of Direct Sum Decomposition of Groups"}

In this article, conservation rules of the direct sum decomposition of groups are mainly discussed. In the first section, we prepare miscellaneous definitions...

Conservation Rules of Direct Sum Decomposition of Groups

Publié en ligne: 31 août 2016

Pages: 81 - 94

Reçu: 31 déc. 2015

DOI: https://doi.org/10.1515/forma-2016-0007

Mots clés
group theory, direct sum decomposition

© by Kazuhisa Nakasho

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

Conservation Rules of Direct Sum Decomposition of Groups

Publié en ligne: 31 août 2016

Pages: 81 - 94

Reçu: 31 déc. 2015

DOI: https://doi.org/10.1515/forma-2016-0007

Mots clésgroup theory, direct sum decomposition

© by Kazuhisa Nakasho

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

Mots clés
group theory, direct sum decomposition