Commit 2023-02-28 19:08 f503fe60

View on Github →

feat: port Data.Real.ENatENNReal (#2529)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Ring/WithTop.lean

Created Mathlib/Data/Real/ENatENNReal.lean

added theorem ENat.map_coe_nnreal

added def ENat.toENNReal

added def ENat.toENNRealOrderEmbedding

added def ENat.toENNRealRingHom

added theorem ENat.toENNReal_add

added theorem ENat.toENNReal_coe

added theorem ENat.toENNReal_le

added theorem ENat.toENNReal_lt

added theorem ENat.toENNReal_max

added theorem ENat.toENNReal_min

added theorem ENat.toENNReal_mono

added theorem ENat.toENNReal_mul

added theorem ENat.toENNReal_ofNat

added theorem ENat.toENNReal_one

added theorem ENat.toENNReal_strictMono

added theorem ENat.toENNReal_sub

added theorem ENat.toENNReal_top

added theorem ENat.toENNReal_zero