ArithmeticFunction.LSeries.term_isMultiplicative_if_fun_isMultiplicative

@[blueprint  "LSeries.term_isMultiplicative_if_fun_isMultiplicative"  (title := "LSeries.term-isMultiplicative-if-fun-isMultiplicative")  (statement := /--    If $f$ is a multiplicative function, then so to is $n\mapsto f(n)/n^s$.  -/)  (proof := /--    Note that $f(mn)/(mn)^s=f(m)f(n)/(m^sn^s)=(f(m)/m^s)(f(n)/n^s)$.  -/)]lemma LSeries.term_isMultiplicative_if_fun_isMultiplicative {f : ℕ → ℂ} (hf : (toArithmeticFunction f).IsMultiplicative) (s : ℂ) {m n : ℕ} (mCn : m.Coprime n) :    LSeries.term f s (m * n) = LSeries.term f s m * LSeries.term f s n := by  simp only [LSeries.term, _root_.mul_eq_zero, cast_mul, mul_ite, mul_zero, ite_mul, zero_mul]  by_cases m_eq_zero : m = 0 <;> simp only [m_eq_zero, true_or, ↓reduceIte, ite_self]  by_cases n_eq_zero : n = 0 <;> simp only [n_eq_zero, or_true, ↓reduceIte]  rw[← mul_div_mul_comm, Complex.natCast_mul_natCast_cpow]  simp only [or_self, ↓reduceIte]  congr 1  simpa [toArithmeticFunction, m_eq_zero, n_eq_zero] using hf.2 mCn