divisor_of_toMeromorphicNFOn — Mathlib

English

Conversion to normal form does not affect the divisor on U; i.e., divisor (toMeromorphicNFOn f U) U = divisor f U.

Русский

Преобразование к нормальной форме не изменяет дивизор на U: divisor (toMeromorphicNFOn f U) U = divisor f U.

LaTeX

$$$\operatorname{divisor}(toMeromorphicNFOn\ f\ U, U) = \operatorname{divisor}(f, U)$$$

Lean4

/-- Conversion of normal form does not affect divisors.
-/
@[simp]
theorem divisor_of_toMeromorphicNFOn (hf : MeromorphicOn f U) : divisor (toMeromorphicNFOn f U) U = divisor f U :=
  by
  ext z
  by_cases hz : z ∈ U <;> simp [hf, (meromorphicNFOn_toMeromorphicNFOn f U).meromorphicOn, hz]

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