one_sub_prime_cpow_ne_zero — Mathlib

English

If p is prime and Re(s) > 1, then 1 − p^(-s) ≠ 0.

Русский

Если p — простое и Re(s) > 1, то 1 − p^(-s) ≠ 0.

LaTeX

$$Let p be a prime and s ∈ ℂ with Re(s) > 1. Then 1 − p^(−s) ≠ 0.$$

Lean4

theorem one_sub_prime_cpow_ne_zero {p : ℕ} (hp : p.Prime) {s : ℂ} (hs : 1 < s.re) : 1 - (p : ℂ) ^ (-s) ≠ 0 :=
  by
  refine sub_ne_zero_of_ne fun H ↦ ?_
  have := norm_prime_cpow_le_one_half ⟨p, hp⟩ hs
  simp only at this
  rw [← H, norm_one] at this
  norm_num at this

Похожие утверждения