ArithmeticFunction.powOfMultiplicative_isMultiplicative

@[blueprint  "powOfMultiplicative_isMultiplicative"  (title := "powOfMultiplicative-isMultiplicative")  (statement := /--    If $f$ is a multiplicative function, then so to is $n\mapsto f(n)^k$ for any $k\in\mathbb{N}$.  -/)  (proof := /--    Note that $f(mn)^k=(f(m)f(n))^k=(f(m)^k)(f(n)^k)$.  -/)]lemma powOfMultiplicative_isMultiplicative {R : Type u_1} [CommMonoidWithZero R]    {f : ArithmeticFunction R} (hf : f.IsMultiplicative) (k : ℕ) :    (toArithmeticFunction (fun n ↦ (f n) ^ k)).IsMultiplicative := by  simp only [IsMultiplicative, toArithmeticFunction, coe_mk, one_ne_zero, ↓reduceIte, _root_.mul_eq_zero, mul_ite, mul_zero, ite_mul, zero_mul, hf.1, one_pow, true_and]  intro m n mCn  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]  simp only [or_self, ↓reduceIte, hf.2 mCn, mul_pow]