ring
n : ℕ
A a b c d u✝ x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t u : ℝ
⊢ -↑u * (↑σ' - 1) + 1 * -(↑t * ↑u) * I = (1 - ↑σ' - ↑t * I) * ↑u
no goals