Theorem: ArithmeticFunction.LSeries_zeta_eulerProduct' (EulerProducts/PNT.lean)

State before:
s : ℂ
hs : 1 < s.re
⊢ cexp (∑' (p : Primes), -(1 - ↑↑p ^ (-s)).log) = L 1 s
Tactic:
convert modOne_eq_one (R := ℂ) ▸ LSeries_eulerProduct' χ₁ hs using 7
State after:
case h.e'_2.h.e'_1.h.e'_5.h.h.e'_3.h.e'_1.h.e'_6
s : ℂ
hs : 1 < s.re
x✝ : Primes
⊢ ↑↑x✝ ^ (-s) = 1 ↑↑x✝ * ↑↑x✝ ^ (-s)

State before:
case h.e'_2.h.e'_1.h.e'_5.h.h.e'_3.h.e'_1.h.e'_6
s : ℂ
hs : 1 < s.re
x✝ : Primes
⊢ ↑↑x✝ ^ (-s) = 1 ↑↑x✝ * ↑↑x✝ ^ (-s)
Tactic:
rw [MulChar.one_apply <| isUnit_of_subsingleton _, one_mul]
State after:
no goals