Commit 2023-09-15 11:27 b449971a
View on Github →feat(Order/WithBot, Data/Real/ENNReal): coe_injective (#7153)
There already exists NNReal.coe_injective
and
WithBot.coe_injective
, so this adds the analogous
ENNReal.coe_injective
and WithTop.injective
.