<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

Published Online: Aug 31, 2016

Page range: 81 - 94

Received: Dec 31, 2015

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

Keywords
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

Published Online: Aug 31, 2016

Page range: 81 - 94

Received: Dec 31, 2015

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

Keywordsgroup theory, direct sum decomposition

© by Kazuhisa Nakasho

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

Keywords
group theory, direct sum decomposition