Commit 2023-02-27 18:08 ab86c6d5

View on Github →

chore: sync Data.Real.ENNReal (#2525)

data.real.ennreal@afdb4fa3b32d41106a4a09b371ce549ad7958abd..57ac39bd365c2f80589a700f9fbb664d3a1a30c2

Estimated changes

Modified Mathlib/Data/Real/ENNReal.lean

deleted theorem ENNReal.coe_nat_le_coe_nat

deleted theorem ENNReal.coe_nat_lt_coe_nat

deleted theorem ENNReal.coe_nat_strictMono

deleted theorem ENNReal.mul_le_mul

deleted theorem ENNReal.one_le_pow_of_one_le

deleted theorem ENNReal.two_ne_zero