Theorem MeromorphicOn.const_smul

Modification history

2026-08-14 09:51

Mathlib/Analysis/Meromorphic/Basic.lean

chore: add tag `fun_prop` to `MeromorphicOn` and `AnalyticOnNhd` (#42570) …

Modified MeromorphicOn.const_smul View on Github →

2026-07-07 22:28

Mathlib/Analysis/Meromorphic/Basic.lean

refactor(Analysis/Meromorphic): generalize 𝕜 → 𝕜 to 𝕜 → 𝕜' for order lemma when possible (#39904) …

Modified MeromorphicOn.const_smul View on Github →

2026-06-22 20:47

Mathlib/Analysis/Meromorphic/Basic.lean

feat(Analysis/Meromorphic): const_smul lemma (#39833) …

Added MeromorphicOn.const_smul View on Github →