Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cyg Structured version   Unicode version

Definition df-cyg 15480
 Description: 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.)
Assertion
Ref Expression
df-cyg CycGrp .g
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-cyg
StepHypRef Expression
1 ccyg 15479 . 2 CycGrp
2 vn . . . . . . 7
3 cz 10274 . . . . . . 7
42cv 1651 . . . . . . . 8
5 vx . . . . . . . . 9
65cv 1651 . . . . . . . 8
7 vg . . . . . . . . . 10
87cv 1651 . . . . . . . . 9
9 cmg 14681 . . . . . . . . 9 .g
108, 9cfv 5446 . . . . . . . 8 .g
114, 6, 10co 6073 . . . . . . 7 .g
122, 3, 11cmpt 4258 . . . . . 6 .g
1312crn 4871 . . . . 5 .g
14 cbs 13461 . . . . . 6
158, 14cfv 5446 . . . . 5
1613, 15wceq 1652 . . . 4 .g
1716, 5, 15wrex 2698 . . 3 .g
18 cgrp 14677 . . 3
1917, 7, 18crab 2701 . 2 .g
201, 19wceq 1652 1 CycGrp .g
 Colors of variables: wff set class This definition is referenced by:  iscyg  15481
 Copyright terms: Public domain W3C validator