Commit 2025-10-28 09:17 9859788e

View on Github →

feat: behavior of divisors when taking powers of meromorphic functions (#30238) Establish the behavior of divisors when taking powers of meromorphic functions. For consistency, provide _fun-versions of several simple lemmas.

Estimated changes

Modified Mathlib/Algebra/Order/WithTop/Untop0.lean

added theorem WithTop.untop₀_natCast

added theorem WithTop.untop₀_ofNat

Modified Mathlib/Analysis/Meromorphic/Divisor.lean

added theorem MeromorphicOn.divisor_const

added theorem MeromorphicOn.divisor_fun_inv

added theorem MeromorphicOn.divisor_fun_mul

added theorem MeromorphicOn.divisor_fun_pow

added theorem MeromorphicOn.divisor_fun_smul

added theorem MeromorphicOn.divisor_fun_zpow

added theorem MeromorphicOn.divisor_intCast

added theorem MeromorphicOn.divisor_natCast

added theorem MeromorphicOn.divisor_ofNat

added theorem MeromorphicOn.divisor_pow

added theorem MeromorphicOn.divisor_zpow

Modified Mathlib/Analysis/Meromorphic/FactorizedRational.lean

Modified Mathlib/Analysis/Meromorphic/Order.lean

added theorem meromorphicOrderAt_const

added theorem meromorphicOrderAt_const_intCast

added theorem meromorphicOrderAt_const_natCast

added theorem meromorphicOrderAt_const_ofNat