Theorem: ζ₁_apply_of_ne_one (EulerProducts/PNT.lean)

State before:
z : ℂ
hz : z ≠ 1
⊢ ζ₁ z = ζ z * (z - 1)
Tactic:
simp [ζ₁, hz]
State after:
no goals