Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-06 07:48 c48d7bfe

View on Github →

feat(data/real/enat_ennreal): define coercion from enat to ennreal (#17207)

Estimated changes

Modified src/algebra/order/ring.lean

added def nat.cast_order_embedding

Modified src/algebra/order/sub/with_top.lean

added theorem with_top.map_sub

Modified src/data/nat/cast.lean

added theorem nat.cast_tsub

Created src/data/real/enat_ennreal.lean

added theorem enat.coe_ennreal_add

added theorem enat.coe_ennreal_bit0

added theorem enat.coe_ennreal_bit1

added theorem enat.coe_ennreal_coe

added theorem enat.coe_ennreal_le

added theorem enat.coe_ennreal_lt

added theorem enat.coe_ennreal_max

added theorem enat.coe_ennreal_min

added theorem enat.coe_ennreal_mono

added theorem enat.coe_ennreal_mul

added theorem enat.coe_ennreal_one

added theorem enat.coe_ennreal_strict_mono

added theorem enat.coe_ennreal_sub

added theorem enat.coe_ennreal_top

added theorem enat.coe_ennreal_zero

added theorem enat.map_coe_nnreal

added def enat.to_ennreal_order_embedding

added def enat.to_ennreal_ring_hom

Modified src/data/real/ennreal.lean

added theorem ennreal.nat_cast_sub