Commit 2024-12-20 13:13 733489d6

View on Github →

feat: add ENat.map and lemmas (#19149)

Estimated changes

Modified Mathlib/Analysis/Analytic/Meromorphic.lean

Modified Mathlib/Data/ENat/Basic.lean

added def ENat.map

added theorem ENat.map_coe

added theorem ENat.map_eq_top_iff

added theorem ENat.map_natCast_nonneg

added theorem ENat.map_ofNat

added theorem ENat.map_one

added theorem ENat.map_top

added theorem ENat.map_zero

added theorem ENat.monotone_map_iff

added theorem ENat.ne_top_iff_exists

added theorem ENat.strictMono_map_iff

Modified Mathlib/Data/Real/ENatENNReal.lean

modified theorem ENat.map_coe_nnreal

modified def ENat.toENNReal

Modified Mathlib/RingTheory/MvPowerSeries/Order.lean