Theorem: LSeries.term_at_one (EulerProducts/EulerProduct.lean)

State before:
f : ℕ → ℂ
h₁ : f 1 = 1
s : ℂ
⊢ term f s 1 = 1
Tactic:
rw [term_of_ne_zero one_ne_zero, h₁, Nat.cast_one, one_cpow, div_one]
State after:
no goals