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

Definition df-dchr 24024
 Description: The group of Dirichlet characters is the set of monoid homomorphisms from to the multiplicative monoid of the complex numbers, equipped with the group operation of pointwise multiplication. (Contributed by Mario Carneiro, 18-Apr-2016.)
Assertion
Ref Expression
df-dchr DChr ℤ/n mulGrp MndHom mulGrpfld Unit
Distinct variable groups:   ,   ,,,

Detailed syntax breakdown of Definition df-dchr
StepHypRef Expression
1 cdchr 24023 . 2 DChr
2 vn . . 3
3 cn 10609 . . 3
4 vz . . . 4
52cv 1436 . . . . 5
6 czn 19005 . . . . 5 ℤ/n
75, 6cfv 5601 . . . 4 ℤ/n
8 vb . . . . 5
94cv 1436 . . . . . . . . . 10
10 cbs 15084 . . . . . . . . . 10
119, 10cfv 5601 . . . . . . . . 9
12 cui 17802 . . . . . . . . . 10 Unit
139, 12cfv 5601 . . . . . . . . 9 Unit
1411, 13cdif 3439 . . . . . . . 8 Unit
15 cc0 9538 . . . . . . . . 9
1615csn 4002 . . . . . . . 8
1714, 16cxp 4852 . . . . . . 7 Unit
18 vx . . . . . . . 8
1918cv 1436 . . . . . . 7
2017, 19wss 3442 . . . . . 6 Unit
21 cmgp 17658 . . . . . . . 8 mulGrp
229, 21cfv 5601 . . . . . . 7 mulGrp
23 ccnfld 18905 . . . . . . . 8 fld
2423, 21cfv 5601 . . . . . . 7 mulGrpfld
25 cmhm 16531 . . . . . . 7 MndHom
2622, 24, 25co 6305 . . . . . 6 mulGrp MndHom mulGrpfld
2720, 18, 26crab 2786 . . . . 5 mulGrp MndHom mulGrpfld Unit
28 cnx 15081 . . . . . . . 8
2928, 10cfv 5601 . . . . . . 7
308cv 1436 . . . . . . 7
3129, 30cop 4008 . . . . . 6
32 cplusg 15152 . . . . . . . 8
3328, 32cfv 5601 . . . . . . 7
34 cmul 9543 . . . . . . . . 9
3534cof 6543 . . . . . . . 8
3630, 30cxp 4852 . . . . . . . 8
3735, 36cres 4856 . . . . . . 7
3833, 37cop 4008 . . . . . 6
3931, 38cpr 4004 . . . . 5
408, 27, 39csb 3401 . . . 4 mulGrp MndHom mulGrpfld Unit
414, 7, 40csb 3401 . . 3 ℤ/n mulGrp MndHom mulGrpfld Unit
422, 3, 41cmpt 4484 . 2 ℤ/n mulGrp MndHom mulGrpfld Unit
431, 42wceq 1437 1 DChr ℤ/n mulGrp MndHom mulGrpfld Unit
 Colors of variables: wff setvar class This definition is referenced by:  dchrval  24025  dchrrcl  24031
 Copyright terms: Public domain W3C validator