Theorem meromorphicOrderAt_fun_prod

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_fun_prodView on Github →
2026-03-26 18:37
Mathlib/Analysis/Meromorphic/Order.lean
feat: add lemmas on (fin)sums and (fin)products of meromorphic functions (#36597) …
Added meromorphicOrderAt_fun_prodView on Github →