Theorem: nterm_eq_norm_term (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℂ
⊢ nterm f σ' n = ‖term f (↑σ') n‖
Tactic:
by_cases h : n = 0 <;> simp [nterm, term, h]
State after:
no goals