Description: Suppose X is a non-principal Dirichlet character with sum_ n e. NN , X ( n ) / n = 0 . Then X is a real character. Part of Lemma 9.4.4 of Shapiro, p. 382. (Contributed by Mario Carneiro, 5-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rpvmasum.z | |
|
rpvmasum.l | |
||
rpvmasum.a | |
||
rpvmasum2.g | |
||
rpvmasum2.d | |
||
rpvmasum2.1 | |
||
rpvmasum2.w | |
||
dchrisum0.b | |
||
Assertion | dchrisum0re | |