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

Definition df-cyg 17501
 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 17500 . 2 CycGrp
2 vn . . . . . . 7
3 cz 10938 . . . . . . 7
42cv 1436 . . . . . . . 8
5 vx . . . . . . . . 9
65cv 1436 . . . . . . . 8
7 vg . . . . . . . . . 10
87cv 1436 . . . . . . . . 9
9 cmg 16660 . . . . . . . . 9 .g
108, 9cfv 5598 . . . . . . . 8 .g
114, 6, 10co 6302 . . . . . . 7 .g
122, 3, 11cmpt 4479 . . . . . 6 .g
1312crn 4851 . . . . 5 .g
14 cbs 15109 . . . . . 6
158, 14cfv 5598 . . . . 5
1613, 15wceq 1437 . . . 4 .g
1716, 5, 15wrex 2776 . . 3 .g
18 cgrp 16657 . . 3
1917, 7, 18crab 2779 . 2 .g
201, 19wceq 1437 1 CycGrp .g
 Colors of variables: wff setvar class This definition is referenced by:  iscyg  17502
 Copyright terms: Public domain W3C validator