Source indexedlemma · leanprover/lean4:v4.32.0

Complex.Hadamard.divisorZeroIndex₀_val_mem_divisor_support

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorIndex · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorIndex.lean:55 to 68

Source documentation

A (nonzero) divisor index has nonzero multiplicity at its underlying point.

Exact Lean statement

@[simp]
lemma divisorZeroIndex₀_val_mem_divisor_support {f : ℂ → ℂ} {U : Set ℂ}
    (p : divisorZeroIndex₀ f U) :
    MeromorphicOn.divisor f U (divisorZeroIndex₀_val p) ≠ 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[simp]lemma divisorZeroIndex₀_val_mem_divisor_support {f : ℂ → ℂ} {U : Set ℂ}    (p : divisorZeroIndex₀ f U) :    MeromorphicOn.divisor f U (divisorZeroIndex₀_val p) ≠ 0 := by  have hn :      Int.toNat (MeromorphicOn.divisor f U (divisorZeroIndex₀_val p)) ≠ 0 := by    intro h0    have q0 : Fin 0 := by      simpa [divisorZeroIndex₀_val, h0] using p.1.2    exact Fin.elim0 q0  intro hdiv  have : Int.toNat (MeromorphicOn.divisor f U (divisorZeroIndex₀_val p)) = 0 := by    simp [hdiv]  exact hn this