Description: The inverse of a Dirichlet character is the conjugate (which is also the multiplicative inverse, because the values of X are unimodular). (Contributed by Mario Carneiro, 28-Apr-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dchrabs.g | |
|
dchrabs.d | |
||
dchrabs.x | |
||
dchrinv.i | |
||
Assertion | dchrinv | |