![]() |
Metamath
Proof Explorer Theorem List (p. 198 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cmnpropd 19701* | If two structures have the same group components (properties), one is a commutative monoid iff the other one is. (Contributed by Mario Carneiro, 6-Jan-2015.) |
โข (๐ โ ๐ต = (Baseโ๐พ)) & โข (๐ โ ๐ต = (Baseโ๐ฟ)) & โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ฅ(+gโ๐พ)๐ฆ) = (๐ฅ(+gโ๐ฟ)๐ฆ)) โ โข (๐ โ (๐พ โ CMnd โ ๐ฟ โ CMnd)) | ||
Theorem | ablpropd 19702* | If two structures have the same group components (properties), one is an Abelian group iff the other one is. (Contributed by NM, 6-Dec-2014.) |
โข (๐ โ ๐ต = (Baseโ๐พ)) & โข (๐ โ ๐ต = (Baseโ๐ฟ)) & โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ฅ(+gโ๐พ)๐ฆ) = (๐ฅ(+gโ๐ฟ)๐ฆ)) โ โข (๐ โ (๐พ โ Abel โ ๐ฟ โ Abel)) | ||
Theorem | ablprop 19703 | If two structures have the same group components (properties), one is an Abelian group iff the other one is. (Contributed by NM, 11-Oct-2013.) |
โข (Baseโ๐พ) = (Baseโ๐ฟ) & โข (+gโ๐พ) = (+gโ๐ฟ) โ โข (๐พ โ Abel โ ๐ฟ โ Abel) | ||
Theorem | iscmnd 19704* | Properties that determine a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.) |
โข (๐ โ ๐ต = (Baseโ๐บ)) & โข (๐ โ + = (+gโ๐บ)) & โข (๐ โ ๐บ โ Mnd) & โข ((๐ โง ๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ฅ + ๐ฆ) = (๐ฆ + ๐ฅ)) โ โข (๐ โ ๐บ โ CMnd) | ||
Theorem | isabld 19705* | Properties that determine an Abelian group. (Contributed by NM, 6-Aug-2013.) |
โข (๐ โ ๐ต = (Baseโ๐บ)) & โข (๐ โ + = (+gโ๐บ)) & โข (๐ โ ๐บ โ Grp) & โข ((๐ โง ๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ฅ + ๐ฆ) = (๐ฆ + ๐ฅ)) โ โข (๐ โ ๐บ โ Abel) | ||
Theorem | isabli 19706* | Properties that determine an Abelian group. (Contributed by NM, 4-Sep-2011.) |
โข ๐บ โ Grp & โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ฅ + ๐ฆ) = (๐ฆ + ๐ฅ)) โ โข ๐บ โ Abel | ||
Theorem | cmnmnd 19707 | A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
โข (๐บ โ CMnd โ ๐บ โ Mnd) | ||
Theorem | cmncom 19708 | A commutative monoid is commutative. (Contributed by Mario Carneiro, 6-Jan-2015.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ CMnd โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ + ๐) = (๐ + ๐)) | ||
Theorem | ablcom 19709 | An Abelian group operation is commutative. (Contributed by NM, 26-Aug-2011.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ Abel โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ + ๐) = (๐ + ๐)) | ||
Theorem | cmn32 19710 | Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ CMnd โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ + ๐) + ๐) = ((๐ + ๐) + ๐)) | ||
Theorem | cmn4 19711 | Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ CMnd โง (๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ + ๐) + (๐ + ๐)) = ((๐ + ๐) + (๐ + ๐))) | ||
Theorem | cmn12 19712 | Commutative/associative law for commutative monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Revised by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ CMnd โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ + (๐ + ๐)) = (๐ + (๐ + ๐))) | ||
Theorem | abl32 19713 | Commutative/associative law for Abelian groups. (Contributed by Stefan O'Rear, 10-Apr-2015.) (Revised by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((๐ + ๐) + ๐) = ((๐ + ๐) + ๐)) | ||
Theorem | cmnmndd 19714 | A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024.) |
โข (๐ โ ๐บ โ CMnd) โ โข (๐ โ ๐บ โ Mnd) | ||
Theorem | cmnbascntr 19715 | The base set of a commutative monoid is its center. (Contributed by SN, 21-Mar-2025.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (Cntrโ๐บ) โ โข (๐บ โ CMnd โ ๐ต = ๐) | ||
Theorem | rinvmod 19716* | Uniqueness of a right inverse element in a commutative monoid, if it exists. Corresponds to caovmo 7647. (Contributed by AV, 31-Dec-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข + = (+gโ๐บ) & โข (๐ โ ๐บ โ CMnd) & โข (๐ โ ๐ด โ ๐ต) โ โข (๐ โ โ*๐ค โ ๐ต (๐ด + ๐ค) = 0 ) | ||
Theorem | ablinvadd 19717 | The inverse of an Abelian group operation. (Contributed by NM, 31-Mar-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข ๐ = (invgโ๐บ) โ โข ((๐บ โ Abel โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐โ(๐ + ๐)) = ((๐โ๐) + (๐โ๐))) | ||
Theorem | ablsub2inv 19718 | Abelian group subtraction of two inverses. (Contributed by Stefan O'Rear, 24-May-2015.) |
โข ๐ต = (Baseโ๐บ) & โข โ = (-gโ๐บ) & โข ๐ = (invgโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((๐โ๐) โ (๐โ๐)) = (๐ โ ๐)) | ||
Theorem | ablsubadd 19719 | Relationship between Abelian group subtraction and addition. (Contributed by NM, 31-Mar-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Abel โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ โ ๐) = ๐ โ (๐ + ๐) = ๐)) | ||
Theorem | ablsub4 19720 | Commutative/associative subtraction law for Abelian groups. (Contributed by NM, 31-Mar-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Abel โง (๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ + ๐) โ (๐ + ๐)) = ((๐ โ ๐) + (๐ โ ๐))) | ||
Theorem | abladdsub4 19721 | Abelian group addition/subtraction law. (Contributed by NM, 31-Mar-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Abel โง (๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ + ๐) = (๐ + ๐) โ (๐ โ ๐) = (๐ โ ๐))) | ||
Theorem | abladdsub 19722 | Associative-type law for group subtraction and addition. (Contributed by NM, 19-Apr-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Abel โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ + ๐) โ ๐) = ((๐ โ ๐) + ๐)) | ||
Theorem | ablsubadd23 19723 | Commutative/associative law for addition and subtraction in abelian groups. (subadd23d 11598 analog.) (Contributed by AV, 2-Mar-2025.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Abel โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ โ ๐) + ๐) = (๐ + (๐ โ ๐))) | ||
Theorem | ablsubaddsub 19724 | Double subtraction and addition in abelian groups. (cnambpcma 46302 analog.) (Contributed by AV, 3-Mar-2025.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Abel โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (((๐ โ ๐) + ๐) โ ๐) = (๐ โ ๐)) | ||
Theorem | ablpncan2 19725 | Cancellation law for subtraction in an Abelian group. (Contributed by NM, 2-Oct-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Abel โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ((๐ + ๐) โ ๐) = ๐) | ||
Theorem | ablpncan3 19726 | A cancellation law for Abelian groups. (Contributed by NM, 23-Mar-2015.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Abel โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ + (๐ โ ๐)) = ๐) | ||
Theorem | ablsubsub 19727 | Law for double subtraction. (Contributed by NM, 7-Apr-2015.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ (๐ โ (๐ โ ๐)) = ((๐ โ ๐) + ๐)) | ||
Theorem | ablsubsub4 19728 | Law for double subtraction. (Contributed by NM, 7-Apr-2015.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((๐ โ ๐) โ ๐) = (๐ โ (๐ + ๐))) | ||
Theorem | ablpnpcan 19729 | Cancellation law for mixed addition and subtraction. (pnpcan 11504 analog.) (Contributed by NM, 29-May-2015.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((๐ + ๐) โ (๐ + ๐)) = (๐ โ ๐)) | ||
Theorem | ablnncan 19730 | Cancellation law for group subtraction. (nncan 11494 analog.) (Contributed by NM, 7-Apr-2015.) |
โข ๐ต = (Baseโ๐บ) & โข โ = (-gโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ (๐ โ (๐ โ ๐)) = ๐) | ||
Theorem | ablsub32 19731 | Swap the second and third terms in a double group subtraction. (Contributed by NM, 7-Apr-2015.) |
โข ๐ต = (Baseโ๐บ) & โข โ = (-gโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((๐ โ ๐) โ ๐) = ((๐ โ ๐) โ ๐)) | ||
Theorem | ablnnncan 19732 | Cancellation law for group subtraction. (nnncan 11500 analog.) (Contributed by NM, 29-Feb-2008.) (Revised by AV, 27-Aug-2021.) |
โข ๐ต = (Baseโ๐บ) & โข โ = (-gโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((๐ โ (๐ โ ๐)) โ ๐) = (๐ โ ๐)) | ||
Theorem | ablnnncan1 19733 | Cancellation law for group subtraction. (nnncan1 11501 analog.) (Contributed by NM, 7-Apr-2015.) |
โข ๐ต = (Baseโ๐บ) & โข โ = (-gโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((๐ โ ๐) โ (๐ โ ๐)) = (๐ โ ๐)) | ||
Theorem | ablsubsub23 19734 | Swap subtrahend and result of group subtraction. (Contributed by NM, 14-Dec-2007.) (Revised by AV, 7-Oct-2021.) |
โข ๐ = (Baseโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Abel โง (๐ด โ ๐ โง ๐ต โ ๐ โง ๐ถ โ ๐)) โ ((๐ด โ ๐ต) = ๐ถ โ (๐ด โ ๐ถ) = ๐ต)) | ||
Theorem | mulgnn0di 19735 | Group multiple of a sum, for nonnegative multiples. (Contributed by Mario Carneiro, 13-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ CMnd โง (๐ โ โ0 โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐))) | ||
Theorem | mulgdi 19736 | Group multiple of a sum. (Contributed by Mario Carneiro, 13-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐))) | ||
Theorem | mulgmhm 19737* | The map from ๐ฅ to ๐๐ฅ for a fixed positive integer ๐ is a monoid homomorphism if the monoid is commutative. (Contributed by Mario Carneiro, 4-May-2015.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) โ โข ((๐บ โ CMnd โง ๐ โ โ0) โ (๐ฅ โ ๐ต โฆ (๐ ยท ๐ฅ)) โ (๐บ MndHom ๐บ)) | ||
Theorem | mulgghm 19738* | The map from ๐ฅ to ๐๐ฅ for a fixed integer ๐ is a group homomorphism if the group is commutative. (Contributed by Mario Carneiro, 4-May-2015.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) โ โข ((๐บ โ Abel โง ๐ โ โค) โ (๐ฅ โ ๐ต โฆ (๐ ยท ๐ฅ)) โ (๐บ GrpHom ๐บ)) | ||
Theorem | mulgsubdi 19739 | Group multiple of a difference. (Contributed by Mario Carneiro, 13-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐ โ ๐)) = ((๐ ยท ๐) โ (๐ ยท ๐))) | ||
Theorem | ghmfghm 19740* | The function fulfilling the conditions of ghmgrp 18986 is a group homomorphism. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
โข ๐ = (Baseโ๐บ) & โข ๐ = (Baseโ๐ป) & โข + = (+gโ๐บ) & โข โจฃ = (+gโ๐ป) & โข ((๐ โง ๐ฅ โ ๐ โง ๐ฆ โ ๐) โ (๐นโ(๐ฅ + ๐ฆ)) = ((๐นโ๐ฅ) โจฃ (๐นโ๐ฆ))) & โข (๐ โ ๐น:๐โontoโ๐) & โข (๐ โ ๐บ โ Grp) โ โข (๐ โ ๐น โ (๐บ GrpHom ๐ป)) | ||
Theorem | ghmcmn 19741* | The image of a commutative monoid ๐บ under a group homomorphism ๐น is a commutative monoid. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
โข ๐ = (Baseโ๐บ) & โข ๐ = (Baseโ๐ป) & โข + = (+gโ๐บ) & โข โจฃ = (+gโ๐ป) & โข ((๐ โง ๐ฅ โ ๐ โง ๐ฆ โ ๐) โ (๐นโ(๐ฅ + ๐ฆ)) = ((๐นโ๐ฅ) โจฃ (๐นโ๐ฆ))) & โข (๐ โ ๐น:๐โontoโ๐) & โข (๐ โ ๐บ โ CMnd) โ โข (๐ โ ๐ป โ CMnd) | ||
Theorem | ghmabl 19742* | The image of an abelian group ๐บ under a group homomorphism ๐น is an abelian group. (Contributed by Mario Carneiro, 12-May-2014.) (Revised by Thierry Arnoux, 26-Jan-2020.) |
โข ๐ = (Baseโ๐บ) & โข ๐ = (Baseโ๐ป) & โข + = (+gโ๐บ) & โข โจฃ = (+gโ๐ป) & โข ((๐ โง ๐ฅ โ ๐ โง ๐ฆ โ ๐) โ (๐นโ(๐ฅ + ๐ฆ)) = ((๐นโ๐ฅ) โจฃ (๐นโ๐ฆ))) & โข (๐ โ ๐น:๐โontoโ๐) & โข (๐ โ ๐บ โ Abel) โ โข (๐ โ ๐ป โ Abel) | ||
Theorem | invghm 19743 | The inversion map is a group automorphism if and only if the group is abelian. (In general it is only a group homomorphism into the opposite group, but in an abelian group the opposite group coincides with the group itself.) (Contributed by Mario Carneiro, 4-May-2015.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ผ = (invgโ๐บ) โ โข (๐บ โ Abel โ ๐ผ โ (๐บ GrpHom ๐บ)) | ||
Theorem | eqgabl 19744 | Value of the subgroup coset equivalence relation on an abelian group. (Contributed by Mario Carneiro, 14-Jun-2015.) |
โข ๐ = (Baseโ๐บ) & โข โ = (-gโ๐บ) & โข โผ = (๐บ ~QG ๐) โ โข ((๐บ โ Abel โง ๐ โ ๐) โ (๐ด โผ ๐ต โ (๐ด โ ๐ โง ๐ต โ ๐ โง (๐ต โ ๐ด) โ ๐))) | ||
Theorem | qusecsub 19745 | Two subgroup cosets are equal if and only if the difference of their representatives is a member of the subgroup. (Contributed by AV, 7-Mar-2025.) |
โข ๐ต = (Baseโ๐บ) & โข โ = (-gโ๐บ) & โข โผ = (๐บ ~QG ๐) โ โข (((๐บ โ Abel โง ๐ โ (SubGrpโ๐บ)) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ([๐] โผ = [๐] โผ โ (๐ โ ๐) โ ๐)) | ||
Theorem | subgabl 19746 | A subgroup of an abelian group is also abelian. (Contributed by Mario Carneiro, 3-Dec-2014.) |
โข ๐ป = (๐บ โพs ๐) โ โข ((๐บ โ Abel โง ๐ โ (SubGrpโ๐บ)) โ ๐ป โ Abel) | ||
Theorem | subcmn 19747 | A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 10-Jan-2015.) |
โข ๐ป = (๐บ โพs ๐) โ โข ((๐บ โ CMnd โง ๐ป โ Mnd) โ ๐ป โ CMnd) | ||
Theorem | submcmn 19748 | A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 24-Apr-2016.) |
โข ๐ป = (๐บ โพs ๐) โ โข ((๐บ โ CMnd โง ๐ โ (SubMndโ๐บ)) โ ๐ป โ CMnd) | ||
Theorem | submcmn2 19749 | A submonoid is commutative iff it is a subset of its own centralizer. (Contributed by Mario Carneiro, 24-Apr-2016.) |
โข ๐ป = (๐บ โพs ๐) & โข ๐ = (Cntzโ๐บ) โ โข (๐ โ (SubMndโ๐บ) โ (๐ป โ CMnd โ ๐ โ (๐โ๐))) | ||
Theorem | cntzcmn 19750 | The centralizer of any subset in a commutative monoid is the whole monoid. (Contributed by Mario Carneiro, 3-Oct-2015.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (Cntzโ๐บ) โ โข ((๐บ โ CMnd โง ๐ โ ๐ต) โ (๐โ๐) = ๐ต) | ||
Theorem | cntzcmnss 19751 | Any subset in a commutative monoid is a subset of its centralizer. (Contributed by AV, 12-Jan-2019.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (Cntzโ๐บ) โ โข ((๐บ โ CMnd โง ๐ โ ๐ต) โ ๐ โ (๐โ๐)) | ||
Theorem | cntrcmnd 19752 | The center of a monoid is a commutative submonoid. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
โข ๐ = (๐ โพs (Cntrโ๐)) โ โข (๐ โ Mnd โ ๐ โ CMnd) | ||
Theorem | cntrabl 19753 | The center of a group is an abelian group. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
โข ๐ = (๐ โพs (Cntrโ๐)) โ โข (๐ โ Grp โ ๐ โ Abel) | ||
Theorem | cntzspan 19754 | If the generators commute, the generated monoid is commutative. (Contributed by Mario Carneiro, 25-Apr-2016.) |
โข ๐ = (Cntzโ๐บ) & โข ๐พ = (mrClsโ(SubMndโ๐บ)) & โข ๐ป = (๐บ โพs (๐พโ๐)) โ โข ((๐บ โ Mnd โง ๐ โ (๐โ๐)) โ ๐ป โ CMnd) | ||
Theorem | cntzcmnf 19755 | Discharge the centralizer assumption in a commutative monoid. (Contributed by Mario Carneiro, 24-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (Cntzโ๐บ) & โข (๐ โ ๐บ โ CMnd) & โข (๐ โ ๐น:๐ดโถ๐ต) โ โข (๐ โ ran ๐น โ (๐โran ๐น)) | ||
Theorem | ghmplusg 19756 | The pointwise sum of two linear functions is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข + = (+gโ๐) โ โข ((๐ โ Abel โง ๐น โ (๐ GrpHom ๐) โง ๐บ โ (๐ GrpHom ๐)) โ (๐น โf + ๐บ) โ (๐ GrpHom ๐)) | ||
Theorem | ablnsg 19757 | Every subgroup of an abelian group is normal. (Contributed by Mario Carneiro, 14-Jun-2015.) |
โข (๐บ โ Abel โ (NrmSGrpโ๐บ) = (SubGrpโ๐บ)) | ||
Theorem | odadd1 19758 | The order of a product in an abelian group divides the LCM of the orders of the factors. (Contributed by Mario Carneiro, 20-Oct-2015.) |
โข ๐ = (odโ๐บ) & โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โ ((๐โ(๐ด + ๐ต)) ยท ((๐โ๐ด) gcd (๐โ๐ต))) โฅ ((๐โ๐ด) ยท (๐โ๐ต))) | ||
Theorem | odadd2 19759 | The order of a product in an abelian group is divisible by the LCM of the orders of the factors divided by the GCD. (Contributed by Mario Carneiro, 20-Oct-2015.) |
โข ๐ = (odโ๐บ) & โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โ ((๐โ๐ด) ยท (๐โ๐ต)) โฅ ((๐โ(๐ด + ๐ต)) ยท (((๐โ๐ด) gcd (๐โ๐ต))โ2))) | ||
Theorem | odadd 19760 | The order of a product is the product of the orders, if the factors have coprime order. (Contributed by Mario Carneiro, 20-Oct-2015.) |
โข ๐ = (odโ๐บ) & โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) = 1) โ (๐โ(๐ด + ๐ต)) = ((๐โ๐ด) ยท (๐โ๐ต))) | ||
Theorem | gex2abl 19761 | A group with exponent 2 (or 1) is abelian. (Contributed by Mario Carneiro, 24-Apr-2016.) |
โข ๐ = (Baseโ๐บ) & โข ๐ธ = (gExโ๐บ) โ โข ((๐บ โ Grp โง ๐ธ โฅ 2) โ ๐บ โ Abel) | ||
Theorem | gexexlem 19762* | Lemma for gexex 19763. (Contributed by Mario Carneiro, 24-Apr-2016.) |
โข ๐ = (Baseโ๐บ) & โข ๐ธ = (gExโ๐บ) & โข ๐ = (odโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ธ โ โ) & โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ฆ โ ๐) โ (๐โ๐ฆ) โค (๐โ๐ด)) โ โข (๐ โ (๐โ๐ด) = ๐ธ) | ||
Theorem | gexex 19763* | In an abelian group with finite exponent, there is an element in the group with order equal to the exponent. In other words, all orders of elements divide the largest order of an element of the group. This fails if ๐ธ = 0, for example in an infinite p-group, where there are elements of arbitrarily large orders (so ๐ธ is zero) but no elements of infinite order. (Contributed by Mario Carneiro, 24-Apr-2016.) |
โข ๐ = (Baseโ๐บ) & โข ๐ธ = (gExโ๐บ) & โข ๐ = (odโ๐บ) โ โข ((๐บ โ Abel โง ๐ธ โ โ) โ โ๐ฅ โ ๐ (๐โ๐ฅ) = ๐ธ) | ||
Theorem | torsubg 19764 | The set of all elements of finite order forms a subgroup of any abelian group, called the torsion subgroup. (Contributed by Mario Carneiro, 20-Oct-2015.) |
โข ๐ = (odโ๐บ) โ โข (๐บ โ Abel โ (โก๐ โ โ) โ (SubGrpโ๐บ)) | ||
Theorem | oddvdssubg 19765* | The set of all elements whose order divides a fixed integer is a subgroup of any abelian group. (Contributed by Mario Carneiro, 19-Apr-2016.) |
โข ๐ = (odโ๐บ) & โข ๐ต = (Baseโ๐บ) โ โข ((๐บ โ Abel โง ๐ โ โค) โ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} โ (SubGrpโ๐บ)) | ||
Theorem | lsmcomx 19766 | Subgroup sum commutes (extended domain version). (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข โ = (LSSumโ๐บ) โ โข ((๐บ โ Abel โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ โ ๐) = (๐ โ ๐)) | ||
Theorem | ablcntzd 19767 | All subgroups in an abelian group commute. (Contributed by Mario Carneiro, 19-Apr-2016.) |
โข ๐ = (Cntzโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) โ โข (๐ โ ๐ โ (๐โ๐)) | ||
Theorem | lsmcom 19768 | Subgroup sum commutes. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) |
โข โ = (LSSumโ๐บ) โ โข ((๐บ โ Abel โง ๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ)) โ (๐ โ ๐) = (๐ โ ๐)) | ||
Theorem | lsmsubg2 19769 | The sum of two subgroups is a subgroup. (Contributed by NM, 4-Feb-2014.) (Proof shortened by Mario Carneiro, 19-Apr-2016.) |
โข โ = (LSSumโ๐บ) โ โข ((๐บ โ Abel โง ๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ)) โ (๐ โ ๐) โ (SubGrpโ๐บ)) | ||
Theorem | lsm4 19770 | Commutative/associative law for subgroup sum. (Contributed by NM, 26-Sep-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
โข โ = (LSSumโ๐บ) โ โข ((๐บ โ Abel โง (๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ)) โง (๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ))) โ ((๐ โ ๐ ) โ (๐ โ ๐)) = ((๐ โ ๐) โ (๐ โ ๐))) | ||
Theorem | prdscmnd 19771 | The product of a family of commutative monoids is commutative. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
โข ๐ = (๐Xs๐ ) & โข (๐ โ ๐ผ โ ๐) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ :๐ผโถCMnd) โ โข (๐ โ ๐ โ CMnd) | ||
Theorem | prdsabld 19772 | The product of a family of Abelian groups is an Abelian group. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
โข ๐ = (๐Xs๐ ) & โข (๐ โ ๐ผ โ ๐) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ :๐ผโถAbel) โ โข (๐ โ ๐ โ Abel) | ||
Theorem | pwscmn 19773 | The structure power on a commutative monoid is commutative. (Contributed by Mario Carneiro, 11-Jan-2015.) |
โข ๐ = (๐ โs ๐ผ) โ โข ((๐ โ CMnd โง ๐ผ โ ๐) โ ๐ โ CMnd) | ||
Theorem | pwsabl 19774 | The structure power on an Abelian group is Abelian. (Contributed by Mario Carneiro, 21-Jan-2015.) |
โข ๐ = (๐ โs ๐ผ) โ โข ((๐ โ Abel โง ๐ผ โ ๐) โ ๐ โ Abel) | ||
Theorem | qusabl 19775 | If ๐ is a subgroup of the abelian group ๐บ, then ๐ป = ๐บ / ๐ is an abelian group. (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข ๐ป = (๐บ /s (๐บ ~QG ๐)) โ โข ((๐บ โ Abel โง ๐ โ (SubGrpโ๐บ)) โ ๐ป โ Abel) | ||
Theorem | abl1 19776 | The (smallest) structure representing a trivial abelian group. (Contributed by AV, 28-Apr-2019.) |
โข ๐ = {โจ(Baseโndx), {๐ผ}โฉ, โจ(+gโndx), {โจโจ๐ผ, ๐ผโฉ, ๐ผโฉ}โฉ} โ โข (๐ผ โ ๐ โ ๐ โ Abel) | ||
Theorem | abln0 19777 | Abelian groups (and therefore also groups and monoids) exist. (Contributed by AV, 29-Apr-2019.) |
โข Abel โ โ | ||
Theorem | cnaddablx 19778 | The complex numbers are an Abelian group under addition. This version of cnaddabl 19779 shows the explicit structure "scaffold" we chose for the definition for Abelian groups. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use; use cnaddabl 19779 instead. (New usage is discouraged.) (Contributed by NM, 18-Oct-2012.) |
โข ๐บ = {โจ1, โโฉ, โจ2, + โฉ} โ โข ๐บ โ Abel | ||
Theorem | cnaddabl 19779 | The complex numbers are an Abelian group under addition. This version of cnaddablx 19778 hides the explicit structure indices i.e. is "scaffold-independent". Note that the proof also does not reference explicit structure indices. The actual structure is dependent on how Base and +g is defined. This theorem should not be referenced in any proof. For the group/ring properties of the complex numbers, see cnring 21168. (Contributed by NM, 20-Oct-2012.) (New usage is discouraged.) |
โข ๐บ = {โจ(Baseโndx), โโฉ, โจ(+gโndx), + โฉ} โ โข ๐บ โ Abel | ||
Theorem | cnaddid 19780 | The group identity element of complex number addition is zero. See also cnfld0 21170. (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 26-Aug-2021.) (New usage is discouraged.) |
โข ๐บ = {โจ(Baseโndx), โโฉ, โจ(+gโndx), + โฉ} โ โข (0gโ๐บ) = 0 | ||
Theorem | cnaddinv 19781 | Value of the group inverse of complex number addition. See also cnfldneg 21172. (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 26-Aug-2021.) (New usage is discouraged.) |
โข ๐บ = {โจ(Baseโndx), โโฉ, โจ(+gโndx), + โฉ} โ โข (๐ด โ โ โ ((invgโ๐บ)โ๐ด) = -๐ด) | ||
Theorem | zaddablx 19782 | The integers are an Abelian group under addition. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use. Use zsubrg 21199 instead. (New usage is discouraged.) (Contributed by NM, 4-Sep-2011.) |
โข ๐บ = {โจ1, โคโฉ, โจ2, + โฉ} โ โข ๐บ โ Abel | ||
Theorem | frgpnabllem1 19783* | Lemma for frgpnabl 19785. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 25-Apr-2024.) |
โข ๐บ = (freeGrpโ๐ผ) & โข ๐ = ( I โWord (๐ผ ร 2o)) & โข โผ = ( ~FG โ๐ผ) & โข + = (+gโ๐บ) & โข ๐ = (๐ฆ โ ๐ผ, ๐ง โ 2o โฆ โจ๐ฆ, (1o โ ๐ง)โฉ) & โข ๐ = (๐ฃ โ ๐ โฆ (๐ โ (0...(โฏโ๐ฃ)), ๐ค โ (๐ผ ร 2o) โฆ (๐ฃ splice โจ๐, ๐, โจโ๐ค(๐โ๐ค)โโฉโฉ))) & โข ๐ท = (๐ โ โช ๐ฅ โ ๐ ran (๐โ๐ฅ)) & โข ๐ = (varFGrpโ๐ผ) & โข (๐ โ ๐ผ โ ๐) & โข (๐ โ ๐ด โ ๐ผ) & โข (๐ โ ๐ต โ ๐ผ) โ โข (๐ โ โจโโจ๐ด, โ โฉโจ๐ต, โ โฉโโฉ โ (๐ท โฉ ((๐โ๐ด) + (๐โ๐ต)))) | ||
Theorem | frgpnabllem2 19784* | Lemma for frgpnabl 19785. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 25-Apr-2024.) |
โข ๐บ = (freeGrpโ๐ผ) & โข ๐ = ( I โWord (๐ผ ร 2o)) & โข โผ = ( ~FG โ๐ผ) & โข + = (+gโ๐บ) & โข ๐ = (๐ฆ โ ๐ผ, ๐ง โ 2o โฆ โจ๐ฆ, (1o โ ๐ง)โฉ) & โข ๐ = (๐ฃ โ ๐ โฆ (๐ โ (0...(โฏโ๐ฃ)), ๐ค โ (๐ผ ร 2o) โฆ (๐ฃ splice โจ๐, ๐, โจโ๐ค(๐โ๐ค)โโฉโฉ))) & โข ๐ท = (๐ โ โช ๐ฅ โ ๐ ran (๐โ๐ฅ)) & โข ๐ = (varFGrpโ๐ผ) & โข (๐ โ ๐ผ โ ๐) & โข (๐ โ ๐ด โ ๐ผ) & โข (๐ โ ๐ต โ ๐ผ) & โข (๐ โ ((๐โ๐ด) + (๐โ๐ต)) = ((๐โ๐ต) + (๐โ๐ด))) โ โข (๐ โ ๐ด = ๐ต) | ||
Theorem | frgpnabl 19785 | The free group on two or more generators is not abelian. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐บ = (freeGrpโ๐ผ) โ โข (1o โบ ๐ผ โ ยฌ ๐บ โ Abel) | ||
Theorem | imasabl 19786* | The image structure of an abelian group is an abelian group (imasgrp 18976 analog). (Contributed by AV, 22-Feb-2025.) |
โข (๐ โ ๐ = (๐น โs ๐ )) & โข (๐ โ ๐ = (Baseโ๐ )) & โข (๐ โ + = (+gโ๐ )) & โข (๐ โ ๐น:๐โontoโ๐ต) & โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ (((๐นโ๐) = (๐นโ๐) โง (๐นโ๐) = (๐นโ๐)) โ (๐นโ(๐ + ๐)) = (๐นโ(๐ + ๐)))) & โข (๐ โ ๐ โ Abel) & โข 0 = (0gโ๐ ) โ โข (๐ โ (๐ โ Abel โง (๐นโ 0 ) = (0gโ๐))) | ||
Syntax | ccyg 19787 | Cyclic group. |
class CycGrp | ||
Definition | df-cyg 19788* | Define a cyclic group, which is a group with an element ๐ฅ, called the generator of the group, such that all elements in the group are multiples of ๐ฅ. A generator is usually not unique. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข CycGrp = {๐ โ Grp โฃ โ๐ฅ โ (Baseโ๐)ran (๐ โ โค โฆ (๐(.gโ๐)๐ฅ)) = (Baseโ๐)} | ||
Theorem | iscyg 19789* | Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) โ โข (๐บ โ CycGrp โ (๐บ โ Grp โง โ๐ฅ โ ๐ต ran (๐ โ โค โฆ (๐ ยท ๐ฅ)) = ๐ต)) | ||
Theorem | iscyggen 19790* | The property of being a cyclic generator for a group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ธ = {๐ฅ โ ๐ต โฃ ran (๐ โ โค โฆ (๐ ยท ๐ฅ)) = ๐ต} โ โข (๐ โ ๐ธ โ (๐ โ ๐ต โง ran (๐ โ โค โฆ (๐ ยท ๐)) = ๐ต)) | ||
Theorem | iscyggen2 19791* | The property of being a cyclic generator for a group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ธ = {๐ฅ โ ๐ต โฃ ran (๐ โ โค โฆ (๐ ยท ๐ฅ)) = ๐ต} โ โข (๐บ โ Grp โ (๐ โ ๐ธ โ (๐ โ ๐ต โง โ๐ฆ โ ๐ต โ๐ โ โค ๐ฆ = (๐ ยท ๐)))) | ||
Theorem | iscyg2 19792* | A cyclic group is a group which contains a generator. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ธ = {๐ฅ โ ๐ต โฃ ran (๐ โ โค โฆ (๐ ยท ๐ฅ)) = ๐ต} โ โข (๐บ โ CycGrp โ (๐บ โ Grp โง ๐ธ โ โ )) | ||
Theorem | cyggeninv 19793* | The inverse of a cyclic generator is a generator. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ธ = {๐ฅ โ ๐ต โฃ ran (๐ โ โค โฆ (๐ ยท ๐ฅ)) = ๐ต} & โข ๐ = (invgโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ ๐ธ) โ (๐โ๐) โ ๐ธ) | ||
Theorem | cyggenod 19794* | An element is the generator of a finite group iff the order of the generator equals the order of the group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ธ = {๐ฅ โ ๐ต โฃ ran (๐ โ โค โฆ (๐ ยท ๐ฅ)) = ๐ต} & โข ๐ = (odโ๐บ) โ โข ((๐บ โ Grp โง ๐ต โ Fin) โ (๐ โ ๐ธ โ (๐ โ ๐ต โง (๐โ๐) = (โฏโ๐ต)))) | ||
Theorem | cyggenod2 19795* | In an infinite cyclic group, the generator must have infinite order, but this property no longer characterizes the generators. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ธ = {๐ฅ โ ๐ต โฃ ran (๐ โ โค โฆ (๐ ยท ๐ฅ)) = ๐ต} & โข ๐ = (odโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ ๐ธ) โ (๐โ๐) = if(๐ต โ Fin, (โฏโ๐ต), 0)) | ||
Theorem | iscyg3 19796* | Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) โ โข (๐บ โ CycGrp โ (๐บ โ Grp โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ โ โค ๐ฆ = (๐ ยท ๐ฅ))) | ||
Theorem | iscygd 19797* | Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ โ ๐ต) & โข ((๐ โง ๐ฆ โ ๐ต) โ โ๐ โ โค ๐ฆ = (๐ ยท ๐)) โ โข (๐ โ ๐บ โ CycGrp) | ||
Theorem | iscygodd 19798 | Show that a group with an element the same order as the group is cyclic. (Contributed by Mario Carneiro, 27-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ (๐โ๐) = (โฏโ๐ต)) โ โข (๐ โ ๐บ โ CycGrp) | ||
Theorem | cycsubmcmn 19799* | The set of nonnegative integer powers of an element ๐ด of a monoid forms a commutative monoid. (Contributed by AV, 20-Jan-2024.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐น = (๐ฅ โ โ0 โฆ (๐ฅ ยท ๐ด)) & โข ๐ถ = ran ๐น โ โข ((๐บ โ Mnd โง ๐ด โ ๐ต) โ (๐บ โพs ๐ถ) โ CMnd) | ||
Theorem | cyggrp 19800 | A cyclic group is a group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข (๐บ โ CycGrp โ ๐บ โ Grp) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |