Commit 2024-01-08 13:15 4fc93c28

View on Github →

chore: Move WithTop lemmas earlier (#9463) Part of #9411

Estimated changes

deleted theorem WithBot.coe_nsmul
added def WithBot.addHom
modified theorem WithBot.bot_ne_nat
added theorem WithBot.coe_addHom
modified theorem WithBot.coe_nat
added theorem WithBot.coe_nsmul
modified theorem WithBot.nat_ne_bot
modified def WithTop.addHom
modified theorem WithTop.coe_add
added theorem WithTop.coe_addHom
modified theorem WithTop.coe_nat
added theorem WithTop.coe_nsmul
modified theorem WithTop.nat_ne_top
modified theorem WithTop.top_ne_nat
modified theorem ENNReal.coe_add