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.

Estimated changes

Modified Mathlib/Data/Real/ENNReal.lean

Modified Mathlib/Order/WithBot.lean

modified theorem WithBot.coe_injective

added theorem WithTop.coe_inj

added theorem WithTop.coe_injective