simp [nterm_eq_norm_term]
case h.e'_5.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hσ : 1 < σ'
i : ℕ
⊢ ‖term f (↑σ') i‖ = nterm f σ' i
no goals