Commit 2024-07-18 16:46 0a87e063

View on Github →

feat(Data.Real.ENatENNReal/EReal): add a few coe lemmas (#14835) Add a few lemmas about coercion:

  • toENNReal_coe_eq_iff, toENNReal_pow in Data.Real.ENatENNReal
  • 9 lemmas about natCast into EReal in Data.Real.EReal Allows a better handle on functions from ENat to ENNReal, as well as from Nat to EReal.

Estimated changes

added theorem ENat.toENNReal_pow
added theorem EReal.natCast_div_le
added theorem EReal.natCast_eq_iff
added theorem EReal.natCast_le_iff
added theorem EReal.natCast_lt_iff
added theorem EReal.natCast_mul
added theorem EReal.natCast_ne_bot
added theorem EReal.natCast_ne_iff
added theorem EReal.natCast_ne_top