Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
Pełny rekord metadanych
Pole DCWartośćJęzyk
dc.contributor.authorCoghetto, Rolandpl
dc.identifier.citationFormalized Mathematics, Volume 23, Issue 2, 127–160pl
dc.description.abstractAbstractWe 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
dc.publisherDe Gruyter Openpl
dc.subjectadditive group;pl
dc.subjectLagrange theorem;pl
dc.subjectnormal subgroup;pl
dc.subjectadditive topological group;pl
dc.subjectadditive abelian group;pl
dc.titleGroups – Additive Notationpl
dc.description.AffiliationRue de la Brasserie 5 7100 La Louvière, Belgiumpl
dc.description.referencesJonathan Backer, Piotr Rudnicki, and Christoph Schwarzweller. Ring ideals. Formalized Mathematics, 9(3):565-582,
dc.description.referencesGrzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382,
dc.description.referencesGrzegorz Bancerek. Cardinal arithmetics. Formalized Mathematics, 1(3):543-547,
dc.description.referencesGrzegorz Bancerek. Tarski’s classes and ranks. Formalized Mathematics, 1(3):563-567,
dc.description.referencesGrzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46,
dc.description.referencesGrzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96,
dc.description.referencesGrzegorz Bancerek. Zermelo theorem and axiom of choice. Formalized Mathematics, 1 (2):265-267,
dc.description.referencesJózef Białas. Group and field definitions. Formalized Mathematics, 1(3):433-439,
dc.description.referencesRichard E. Blahut. Cryptography and Secure Communication. Cambridge University Press,
dc.description.referencesSylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Formalization of real analysis: A survey of proof assistants and libraries. Mathematical Structures in Computer Science, pages 1-38,
dc.description.referencesNicolas Bourbaki. General Topology: Chapters 1-4. Springer Science and Business Media,
dc.description.referencesCzesław Bylinski. Binary operations. Formalized Mathematics, 1(1):175-180,
dc.description.referencesCzesław Bylinski. Binary operations applied to finite sequences. Formalized Mathematics, 1(4):643-649,
dc.description.referencesCzesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65,
dc.description.referencesCzesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164,
dc.description.referencesCzesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367,
dc.description.referencesCzesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53,
dc.description.referencesAgata Darmochwał. Compact spaces. Formalized Mathematics, 1(2):383-386,
dc.description.referencesAgata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167,
dc.description.referencesAgata Darmochwał. Families of subsets, subspaces and mappings in topological spaces. Formalized Mathematics, 1(2):257-261,
dc.description.referencesYuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Z-modules. Formalized Mathematics, 20(1):47-59, 2012. doi:10.2478/v10037-012-0007-z. [Crossref]pl
dc.description.referencesEdwin Hewitt and Kenneth A. Ross. Abstract Harmonic Analysis: Volume I. Structure of Topological Groups. Integration. Theory Group Representations, volume 115. Springer Science and Business Media,
dc.description.referencesJohannes Hölzl, Fabian Immler, and Brian Huffman. Type classes and filters for mathematical analysis in Isabelle/HOL. In Interactive Theorem Proving, pages 279-294. Springer,
dc.description.referencesTeturo Inui, Yukito Tanabe, and Yositaka Onodera. Group theory and its applications in physics, volume 78. Springer Science and Business Media,
dc.description.referencesArtur Korniłowicz. The definition and basic properties of topological groups. Formalized Mathematics, 7(2):217-225,
dc.description.referencesRafał Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relatively primes. Formalized Mathematics, 1(5):829-832,
dc.description.referencesChristopher Norman. Basic theory of additive Abelian groups. In Finitely Generated Abelian Groups and Similarity of Matrices over a Field, Springer Undergraduate Mathematics Series, pages 47-96. Springer, 2012. ISBN 978-1-4471-2729-1. doi:10.1007/978-1-4471-2730-7 2. [Crossref]pl
dc.description.referencesBeata Padlewska. Locally connected spaces. Formalized Mathematics, 2(1):93-96,
dc.description.referencesBeata Padlewska. Families of sets. Formalized Mathematics, 1(1):147-152,
dc.description.referencesBeata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223-230,
dc.description.referencesAlexander Yu. Shibakov and Andrzej Trybulec. The Cantor set. Formalized Mathematics, 5(2):233-236,
dc.description.referencesAndrzej Trybulec. A Borsuk theorem on homotopy types. Formalized Mathematics, 2(4): 535-545,
dc.description.referencesAndrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1): 115-122,
dc.description.referencesAndrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25-34,
dc.description.referencesAndrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97-105,
dc.description.referencesAndrzej Trybulec. On the sets inhabited by numbers. Formalized Mathematics, 11(4): 341-347,
dc.description.referencesAndrzej Trybulec. Semilattice operations on finite subsets. Formalized Mathematics, 1 (2):369-376,
dc.description.referencesAndrzej Trybulec. Baire spaces, Sober spaces. Formalized Mathematics, 6(2):289-294,
dc.description.referencesAndrzej Trybulec and Agata Darmochwał. Boolean domains. Formalized Mathematics, 1 (1):187-190,
dc.description.referencesMichał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505,
dc.description.referencesWojciech A. Trybulec. Groups. Formalized Mathematics, 1(5):821-827,
dc.description.referencesWojciech A. Trybulec. Subgroup and cosets of subgroups. Formalized Mathematics, 1(5): 855-864,
dc.description.referencesWojciech A. Trybulec. Classes of conjugation. Normal subgroups. Formalized Mathematics, 1(5):955-962,
dc.description.referencesWojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296,
dc.description.referencesZinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71,
dc.description.referencesEdmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83,
dc.description.referencesEdmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186,
dc.description.referencesMirosław Wysocki and Agata Darmochwał. Subsets of topological spaces. Formalized Mathematics, 1(1):231-237,
Występuje w kolekcji(ach):Formalized Mathematics, 2015, Volume 23, Issue 2

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma-2015-0013.pdf363,52 kBAdobe PDFOtwórz
Pokaż uproszczony widok rekordu Zobacz statystyki

Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons