Theorem meromorphicOrderAt_const_natCast

Modification history

2026-07-07 22:28
Mathlib/Analysis/Meromorphic/Order.lean
refactor(Analysis/Meromorphic): generalize 𝕜 → 𝕜 to 𝕜 → 𝕜' for order lemma when possible (#39904) …
Modified meromorphicOrderAt_const_natCastView on Github →
2025-10-28 09:17
Mathlib/Analysis/Meromorphic/Order.lean
feat: behavior of divisors when taking powers of meromorphic functions (#30238) …
Added meromorphicOrderAt_const_natCastView on Github →