Theorem: term_prod_at_zero (Ray/Dynamics/BottcherNear.lean)

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ tprodOn (term f d) 0 = 1
Tactic:
simp_rw [tprodOn, term_at_zero s, tprod_one]
State after:
no goals