R : Type ?u.546111
k : ℕ
⊢ IsMultiplicative (ζ * pow k)
R : Type ?u.546111
k : ℕ
⊢ IsMultiplicative (σ k)
rw [← zeta_mul_pow_eq_sigma]
no goals
R : Type ?u.546111
k : ℕ
⊢ IsMultiplicative (ζ * pow k)
apply isMultiplicative_zeta.mul isMultiplicative_pow