Theorem: DirichletCharacter.toFun_on_nat_map_mul (EulerProducts/DirichletLSeries.lean)

State before:
N : ℕ
χ : DirichletCharacter ℂ N
m n : ℕ
⊢ (fun n => χ ↑n) (m * n) = (fun n => χ ↑n) m * (fun n => χ ↑n) n
Tactic:
simp only [cast_mul, map_mul]
State after:
no goals