theorem DirichletCharacter.star_eq_self_of_sq_eq_one {q : ℕ} (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) : star χ = χ

Complex conjugation fixes a quadratic Dirichlet character.

theorem DirichletCharacter.conj_sum_range_cpowWeight_character_of_sq_eq_one {q : ℕ} (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) (s : ℂ) (n : ℕ) : (starRingEnd ℂ) (∑ k ∈ Finset.range n, DirichletLAbelWeightVariation.cpowWeight s ↑k * χ ↑k) = ∑ k ∈ Finset.range n, DirichletLAbelWeightVariation.cpowWeight ((starRingEnd ℂ) s) ↑k * χ ↑k

Conjugating a finite natural-order partial sum conjugates its parameter.

theorem DirichletCharacter.LFunction_conj_eq_conj_LFunction_of_sq_eq_one {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hquad : χ ^ 2 = 1) (s : ℂ) (hs : 0 < s.re) : LFunction χ ((starRingEnd ℂ) s) = (starRingEnd ℂ) (LFunction χ s)

A nonprincipal quadratic Dirichlet L-function commutes with complex conjugation throughout re s > 0. The proof compares the natural-order partial sums and then uses continuity and uniqueness of limits.

theorem DirichletCharacter.LFunction_ofReal_im_eq_zero_of_sq_eq_one {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hquad : χ ^ 2 = 1) (β : ℝ) (hβ : 0 < β) : (LFunction χ ↑β).im = 0

Every positive real value of a nonprincipal quadratic Dirichlet L-function is real.

theorem DirichletCharacter.LFunction_conj_eq_zero_of_sq_eq_one {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hquad : χ ^ 2 = 1) (s : ℂ) (hs : 0 < s.re) (hz : LFunction χ s = 0) : LFunction χ ((starRingEnd ℂ) s) = 0

Zeros of a nonprincipal quadratic Dirichlet L-function in re s > 0 are closed under complex conjugation.