theorem
DirichletCharacter.inv_eq_self_of_sq_eq_one
{N : ℕ}
{χ : DirichletCharacter ℂ N}
(hquad : χ ^ 2 = 1)
:
A multiplicative quadratic character is self-inverse.
theorem
DirichletCharacter.IsPrimitive.completedLFunction_one_sub_quadratic
{N : ℕ}
[NeZero N]
{χ : DirichletCharacter ℂ N}
(hχ : χ.IsPrimitive)
(hquad : χ ^ 2 = 1)
(s : ℂ)
:
The primitive functional equation specialized to a quadratic character.
theorem
DirichletCharacter.IsPrimitive.norm_rootNumber_of_quadratic
{N : ℕ}
[NeZero N]
{χ : DirichletCharacter ℂ N}
(hχ : χ.IsPrimitive)
(_hquad : χ ^ 2 = 1)
:
The root number in the primitive quadratic lane has norm one.