Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.kadiri_one_div_sub_one_meromorphicAt_one

PrimeNumberTheoremAnd.IEANTN.KadiriEq12Foundations · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Foundations.lean:685 to 692

Mathematical statement

Exact Lean statement

lemma kadiri_one_div_sub_one_meromorphicAt_one :
    MeromorphicAt (fun s : ℂ => (1 : ℂ) / (s - 1)) (1 : ℂ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma kadiri_one_div_sub_one_meromorphicAt_one :    MeromorphicAt (fun s : ℂ => (1 : ℂ) / (s - 1)) (1 : ℂ) := by  have hnum : MeromorphicAt (fun _ : ℂ => (1 : ℂ)) (1 : ℂ) :=    MeromorphicAt.const (1 : ℂ) (1 : ℂ)  have hden : MeromorphicAt (fun s : ℂ => s - 1) (1 : ℂ) := by    exact (show AnalyticAt ℂ (fun s : ℂ => s - 1) (1 : ℂ) from by fun_prop).meromorphicAt  change MeromorphicAt ((fun _ : ℂ => (1 : ℂ)) / fun s : ℂ => s - 1) (1 : ℂ)  exact hnum.div hden