Theorem: DirichletCharacter.toFun_on_nat_map_one (EulerProducts/EulerProduct.lean)

State before:
N : ℕ
χ : DirichletCharacter ℂ N
⊢ (fun n => χ ↑n) 1 = 1
Tactic:
simp only [cast_one, map_one]
State after:
no goals