dsimp [MellinTransform, MellinConvolution]
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
⊢ 𝓜 (MellinConvolution f g) s = 𝓜 f s * 𝓜 g s
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioi 0, (∫ (y : ℝ) in Ioi 0, f y * g (x / y) / ↑y) * ↑x ^ (s - 1) =
    (∫ (x : ℝ) in Ioi 0, f x * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)