Theorem: DirichletCharacter.LSeries_eulerProduct (EulerProducts/EulerProduct.lean)

State before:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - χ ↑p * ↑p ^ (-s))⁻¹) atTop (𝓝 (L (fun n => χ ↑n) s))
Tactic:
refine Tendsto.congr (fun n ↦ Finset.prod_congr rfl fun p hp ↦ ?_) <|
  eulerProduct_of_completelyMultiplicative (toFun_on_nat_map_one χ) (toFun_on_nat_map_mul χ) <|
  LSeriesSummable_of_one_lt_re χ hs
State after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
n p : ℕ
hp : p ∈ n.primesBelow
⊢ (1 - term (fun n => χ ↑n) s p)⁻¹ = (1 - χ ↑p * ↑p ^ (-s))⁻¹

State before:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
n p : ℕ
hp : p ∈ n.primesBelow
⊢ (1 - term (fun n => χ ↑n) s p)⁻¹ = (1 - χ ↑p * ↑p ^ (-s))⁻¹
Tactic:
rw [term_of_ne_zero (prime_of_mem_primesBelow hp).ne_zero, cpow_neg, div_eq_mul_inv]
State after:
no goals