Theorem MeromorphicOn.smul

Modification history

2026-01-27 20:37

Mathlib/Analysis/Meromorphic/Basic.lean

feat(Analysis/SpecialFunctions/Complex/LogDeriv): meromorphicity of `logDeriv` (#34456) …

Modified MeromorphicOn.smul View on Github →

2025-12-22 21:59

Mathlib/Analysis/Meromorphic/Basic.lean

refactor: use "@[to_fun]" to generate some lemmas (#32830)

Modified MeromorphicOn.smul View on Github →

2024-02-06 13:53

Mathlib/Analysis/Analytic/Meromorphic.lean

feat(Analysis/Analytic/Meromorphic): more API for meromorphic functions (#9621) …

Added MeromorphicOn.smul View on Github →