Theorem Meromorphic.const_smul

Modification history

2026-07-07 22:28
Mathlib/Analysis/Meromorphic/Basic.lean
refactor(Analysis/Meromorphic): generalize 𝕜 → 𝕜 to 𝕜 → 𝕜' for order lemma when possible (#39904) …
Modified Meromorphic.const_smulView on Github →
2026-06-22 20:47
Mathlib/Analysis/Meromorphic/Basic.lean
feat(Analysis/Meromorphic): const_smul lemma (#39833) …
Added Meromorphic.const_smulView on Github →