<abstract xmlns="http://www.w3.org/1999/xhtml">We translate the articles covering group theory already available in the Mizar Mathematical Library from multiplicative into additive notation. We adapt the works of Wojciech A. Trybulec [41, 42, 43] and Artur Korniłowicz [25]. In particular, these authors have defined the notions of group, abelian group, power of an element of a group, order of a group and order of an element, subgroup, coset of a subgroup, index of a subgroup, conjugation, normal subgroup, topological group, dense subset and basis of a topological group. Lagrange’s theorem and some other theorems concerning these notions [9, 24, 22] are presented. Note that “The term ℤ-module is simply another name for an additive abelian group” [27]. We take an approach different than that used by Futa et al. [21] to use in a future article the results obtained by Artur Korniłowicz [25]. Indeed, Hölzl et al. showed that it was possible to build “a generic theory of limits based on filters” in Isabelle/HOL [23, 10]. Our goal is to define the convergence of a sequence and the convergence of a series in an abelian topological group [11] using the notion of filters.</abstract>

We translate the articles covering group theory already available in the Mizar Mathematical Library from multiplicative into additive notation. We adapt the works of Wojciech A. Trybulec [41, 42, 43] and Artur Korniłowicz [25]. In particular, these authors have defined the notions of group, abelian group, power of an element of a group, order of a group and order of an element, subgroup, coset of a subgroup, index of a subgroup, conjugation, normal subgroup, topological group, dense subset and basis of a topological group. Lagrange’s theorem and some other theorems concerning these notions [9, 24, 22] are presented. Note that “The term ℤ-module is simply another name for an additive abelian group” [27]. We take an approach different than that used by Futa et al. [21] to use in a future article the results obtained by Artur Korniłowicz [25]. Indeed, Hölzl et al. showed that it was possible to build “a generic theory of limits based on filters” in Isabelle/HOL [23, 10]. Our goal is to define the convergence of a sequence and the convergence of a series in an abelian topological group [11] using the notion of filters.

Groups – Additive Notation

Rue de la Brasserie 5 7100 La Louvière, Belgium

Formalized Mathematics

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

{"article-title":"Groups \u2013 Additive Notation"}

We translate the articles covering group theory already available in the Mizar Mathematical Library from multiplicative into additive notation. We adapt the...

Groups – Additive Notation

Data publikacji: 13 sie 2015

Zakres stron: 127 - 160

Otrzymano: 30 kwi 2015

DOI: https://doi.org/10.1515/forma-2015-0013

Słowa kluczowe
additive group, subgroup, Lagrange theorem, conjugation, normal subgroup, index, additive topological group, basis, neighborhood, additive abelian group, Z-module

© by Roland Coghetto

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

Groups – Additive Notation

Data publikacji: 13 sie 2015

Zakres stron: 127 - 160

Otrzymano: 30 kwi 2015

DOI: https://doi.org/10.1515/forma-2015-0013

Słowa kluczoweadditive group, subgroup, Lagrange theorem, conjugation, normal subgroup, index, additive topological group, basis, neighborhood, additive abelian group, Z-module

© by Roland Coghetto

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

Słowa kluczowe
additive group, subgroup, Lagrange theorem, conjugation, normal subgroup, index, additive topological group, basis, neighborhood, additive abelian group, Z-module