case zero
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : IsMultiplicative f
⊢ IsMultiplicative (ArithmeticFunction.ppow f Nat.zero)

case succ
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : IsMultiplicative f
k : ℕ
hi : IsMultiplicative (ArithmeticFunction.ppow f k)
⊢ IsMultiplicative (ArithmeticFunction.ppow f (succ k))
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : IsMultiplicative f
k : ℕ
⊢ IsMultiplicative (ArithmeticFunction.ppow f k)
induction' k with k hi
no goals
case zero
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : IsMultiplicative f
⊢ IsMultiplicative (ArithmeticFunction.ppow f Nat.zero)
exact isMultiplicative_zeta.nat_cast
case succ
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : IsMultiplicative f
k : ℕ
hi : IsMultiplicative (ArithmeticFunction.ppow f k)
⊢ IsMultiplicative (ArithmeticFunction.pmul f (ArithmeticFunction.ppow f k))
case succ
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : IsMultiplicative f
k : ℕ
hi : IsMultiplicative (ArithmeticFunction.ppow f k)
⊢ IsMultiplicative (ArithmeticFunction.ppow f (succ k))
rw [ppow_succ]
no goals
case succ
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : IsMultiplicative f
k : ℕ
hi : IsMultiplicative (ArithmeticFunction.ppow f k)
⊢ IsMultiplicative (ArithmeticFunction.pmul f (ArithmeticFunction.ppow f k))
apply hf.pmul hi