ring
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ 1 / ε * x ^ (1 / ε - 1) * (Ψ (x ^ (1 / ε)) / x ^ (1 / ε)) = Ψ (x ^ (1 / ε)) / x ^ (1 / ε) * x ^ (1 / ε - 1) * (1 / ε)
no goals