Commit 2026-09-01 23:57 cf0910d5

View on Github →

feat: Invariance of meromorphicity under scaling (#41303) Prove that various notions associated with meromorphic functions are invariant under scaling. Add several missing fun_prop tags and normalize comments.

Estimated changes

Modified Mathlib/Analysis/Analytic/Constructions.lean

added theorem analyticAt_zero

Modified Mathlib/Analysis/Meromorphic/Basic.lean

added theorem MeromorphicOn.meromorphicOn_const_smul_iff_meromorphicOn

added theorem meromorphicAt_const_smul_iff_meromorphicAt

added theorem meromorphic_const_smul_iff_meromorphic

Modified Mathlib/Analysis/Meromorphic/Divisor.lean

added theorem MeromorphicOn.divisor_const_smul

Modified Mathlib/Analysis/Meromorphic/NormalForm.lean

modified theorem AnalyticAt.meromorphicNFAt

modified theorem MeromorphicNFAt.inv

modified theorem MeromorphicNFAt.meromorphicAt

added theorem MeromorphicNFAt.smul_const

added theorem meromorphicNFAt_const_smul_iff_meromorphicNFAt

added theorem meromorphicNFOn_const_smul_iff_meromorphicNFOn

Modified Mathlib/Analysis/Meromorphic/Order.lean

added theorem meromorphicOrderAt_const_smul_eq_meromorphicOrderAt