divisor_inv — Mathlib

English

The divisor of the inverse is the negative of the divisor.

Русский

Делитель обратной функции равен противоположному делителю.

LaTeX

$$$\text{divisor}(f^{-1}, U) = -\text{divisor}(f, U)$$$

Lean4

/-- The divisor of the inverse is the negative of the divisor. -/
@[simp]
theorem divisor_inv {f : 𝕜 → 𝕜} : divisor f⁻¹ U = -divisor f U :=
  by
  ext z
  by_cases h : MeromorphicOn f U ∧ z ∈ U
  · simp [divisor_apply, h, meromorphicOrderAt_inv]
  · simp [divisor_def, h]

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