divisor_def — Mathlib

English

If f is meromorphic on U and z ∈ U, then the divisor at z equals meromorphicOrderAt(f,z) untop₀.

Русский

Если f мероморфна на U и z ∈ U, то делитель в точке z равен meromorphicOrderAt(f,z) untop₀.

LaTeX

$$$\text{MeromorphicOn}(f, U) \land z \in U \Rightarrow \text{divisor}(f, U)(z) = (meromorphicOrderAt(f, z)).untop_0$$$

Lean4

/-- Definition of the divisor -/
theorem divisor_def (f : 𝕜 → E) (U : Set 𝕜) :
    divisor f U z = if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0 :=
  rfl

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