no goals
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
⊢ ↑(ArithmeticFunction.pmul f g) 1 = 1
simp [hf, hg]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ↑f m * ↑f n * (↑g m * ↑g n) = ↑f m * ↑g m * (↑f n * ↑g n)
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ↑(ArithmeticFunction.pmul f g) (m * n) = ↑(ArithmeticFunction.pmul f g) m * ↑(ArithmeticFunction.pmul f g) n
simp only [pmul_apply, hf.map_mul_of_coprime cop, hg.map_mul_of_coprime cop]
no goals
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ↑f m * ↑f n * (↑g m * ↑g n) = ↑f m * ↑g m * (↑f n * ↑g n)
ring