ArithmeticFunction.isMultiplicative_powR

@[blueprint  "isMultiplicative_powR"  (title := "isMultiplicative-powR")  (statement := /--    For fixed $\nu$ the function $n\mapsto n^\nu$ is multiplicative.  -/)  (proof := /--    This immediately follows from the fact that exponentiation with a fixed power is a homomorphism.  -/)]theorem isMultiplicative_powR {ν : ℂ} : IsMultiplicative (powR ν) := by  refine ⟨by simp [powR], fun {m n : ℕ} mCn => ?_⟩  simp only [powR, ArithmeticFunction.coe_mk]  rcases Nat.eq_zero_or_pos m with rfl | hm  · simp only [zero_mul, ↓reduceIte, mul_ite, mul_zero, ite_self]  rcases Nat.eq_zero_or_pos n with rfl | hn  · simp only [mul_zero, ↓reduceIte]  have hmn_pos : m * n ≠ 0 := Nat.mul_ne_zero hm.ne' hn.ne'  simp only [hm.ne', hn.ne', hmn_pos, if_false]  push_cast  exact Complex.natCast_mul_natCast_cpow m n ν