Metamath Proof Explorer


Definition df-dchr

Description: The group of Dirichlet characters mod n is the set of monoid homomorphisms from ZZ / n ZZ to the multiplicative monoid of the complex numbers, equipped with the group operation of pointwise multiplication. (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Assertion df-dchr DChr = n /n / z x mulGrp z MndHom mulGrp fld | Base z Unit z × 0 x / b Base ndx b + ndx f × b × b

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdchr class DChr
1 vn setvar n
2 cn class
3 czn class ℤ/nℤ
4 1 cv setvar n
5 4 3 cfv class /n
6 vz setvar z
7 vx setvar x
8 cmgp class mulGrp
9 6 cv setvar z
10 9 8 cfv class mulGrp z
11 cmhm class MndHom
12 ccnfld class fld
13 12 8 cfv class mulGrp fld
14 10 13 11 co class mulGrp z MndHom mulGrp fld
15 cbs class Base
16 9 15 cfv class Base z
17 cui class Unit
18 9 17 cfv class Unit z
19 16 18 cdif class Base z Unit z
20 cc0 class 0
21 20 csn class 0
22 19 21 cxp class Base z Unit z × 0
23 7 cv setvar x
24 22 23 wss wff Base z Unit z × 0 x
25 24 7 14 crab class x mulGrp z MndHom mulGrp fld | Base z Unit z × 0 x
26 vb setvar b
27 cnx class ndx
28 27 15 cfv class Base ndx
29 26 cv setvar b
30 28 29 cop class Base ndx b
31 cplusg class + 𝑔
32 27 31 cfv class + ndx
33 cmul class ×
34 33 cof class f ×
35 29 29 cxp class b × b
36 34 35 cres class f × b × b
37 32 36 cop class + ndx f × b × b
38 30 37 cpr class Base ndx b + ndx f × b × b
39 26 25 38 csb class x mulGrp z MndHom mulGrp fld | Base z Unit z × 0 x / b Base ndx b + ndx f × b × b
40 6 5 39 csb class /n / z x mulGrp z MndHom mulGrp fld | Base z Unit z × 0 x / b Base ndx b + ndx f × b × b
41 1 2 40 cmpt class n /n / z x mulGrp z MndHom mulGrp fld | Base z Unit z × 0 x / b Base ndx b + ndx f × b × b
42 0 41 wceq wff DChr = n /n / z x mulGrp z MndHom mulGrp fld | Base z Unit z × 0 x / b Base ndx b + ndx f × b × b