Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/4877
Tytuł: | Groups – Additive Notation |
Autorzy: | Coghetto, Roland |
Słowa kluczowe: | additive group; subgroup; Lagrange theorem; conjugation; normal subgroup; index; additive topological group; basis; neighborhood; additive abelian group; Z-module |
Data wydania: | 2015 |
Data dodania: | 15-gru-2016 |
Wydawca: | De Gruyter Open |
Źródło: | Formalized Mathematics, Volume 23, Issue 2, 127–160 |
Abstrakt: | AbstractWe 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. |
Afiliacja: | Rue de la Brasserie 5 7100 La Louvière, Belgium |
URI: | http://hdl.handle.net/11320/4877 |
DOI: | 10.1515/forma-2015-0013 |
ISSN: | 1426-2630 1898-9934 |
Typ Dokumentu: | Article |
Występuje w kolekcji(ach): | Formalized Mathematics, 2015, Volume 23, Issue 2 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
forma-2015-0013.pdf | 363,52 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL