divisor_nonneg — Mathlib

English

Second simplified form of divisor congruence on codiscreteWithin.

Русский

Вторая упрощённая форма конгруэнтности делителя на codiscreteWithin.

LaTeX

$$$\text{MeromorphicOn}(f_1, U) \Rightarrow (f_1 =\!\!\!\!_{\text{codiscreteWithin }U} f_2) \Rightarrow \text{divisor}(f_1, U) = \text{divisor}(f_2, U)$$$

Lean4

/-- Analytic functions have non-negative divisors. -/
theorem divisor_nonneg {f : 𝕜 → E} (hf : AnalyticOnNhd 𝕜 f U) : 0 ≤ MeromorphicOn.divisor f U :=
  by
  intro x
  by_cases hx : x ∈ U
  · simp [hf.meromorphicOn, hx, (hf x hx).meromorphicOrderAt_nonneg]
  simp [hx]

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