Theorem: MellinTransform_eq (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
⊢ 𝓜 = mellin
Tactic:
unfold mellin MellinTransform
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
⊢ (fun f s => ∫ (x : ℝ) in Ioi 0, f x * ↑x ^ (s - 1)) = fun f s => ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f t

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
⊢ (fun f s => ∫ (x : ℝ) in Ioi 0, f x * ↑x ^ (s - 1)) = fun f s => ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f t
Tactic:
simp_rw [smul_eq_mul, mul_comm]
State after:
no goals