Groups -- additive notation.

DOI10.1515/FORMA-2015-0013MaRDI QIDQ491777zbMATH OpenOpenAlexFDO

Authors Roland Coghetto

Publication date 19 August 2015

Published in Formalized Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported

Full work available at URL https://doi.org/10.1515/forma-2015-0013

zbMATH Keywords

indexbasesnormal subgroupsconjugationneighborhoodsformalizationLagrange theorem\(\mathbb Z\)-modulesadditive Abelian groupsadditive groupsadditive topological groups

Mathematics Subject Classification ID

Structure of general topological groups (22A05) Mechanization of proofs and logical operations (03B35) Axiomatics and elementary properties of groups (20A05)

Recommendations

• Summable family in a commutative group
• Σ-Groups as Convergence Groups
• scientific article; zbMATH DE number 2186692
• TOPOLOGIES ON ABELIAN GROUPS
• scientific article; zbMATH DE number 3929075

Cites work

• scientific article; zbMATH DE number 3647508 (Why is no real title available?)
• scientific article; zbMATH DE number 42091 (Why is no real title available?)
• scientific article; zbMATH DE number 4197282 (Why is no real title available?)
• Finitely Generated Abelian Groups and Similarity of Matrices over a Field
• Formalization of real analysis: a survey of proof assistants and libraries
• Group theory and its applications in physics. Transl. by the authors from the Japanese.
• Semantics of MML query -- ordering
• Type classes and filters for mathematical analysis in Isabelle/HOL
• \(\mathbb Z\)-modules

Cited in

(1)

• Summable family in a commutative group

Describes a project that uses

Uses Software

• Mizar
• Isabelle/HOL

This page was built for publication: Groups -- additive notation.

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q491777)