logCounting_coe — Mathlib

English

For finite a0, logCounting f a0 equals the logCounting of the divisor of f − a0.

Русский

Для конечного a0 logCounting f a0 равно logCounting делителя f − a0.

LaTeX

$$$\logCounting f a_0 = (\text{divisor }(f- a_0)\ univ)^{+}.\logCounting$$$

Lean4

/-- For finite values `a₀`, the logarithmic counting function `logCounting f a₀` is the counting
function associated with the zero-divisor of the meromorphic function `f - a₀`.
-/
theorem logCounting_coe : logCounting f a₀ = (divisor (fun z ↦ f z - a₀) univ)⁺.logCounting := by simp [logCounting]

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