Commit 2024-02-12 08:25 bc539a7b

View on Github →

feat: Complete NNReal coercion lemmas (#10214) Add a few missing lemmas about the coercion NNReal → Real. Remove a bunch of protected on the existing coercion lemmas (so that it matches the convention for other coercions). Rename NNReal.coe_eq to NNReal.coe_inj From LeanAPAP

Estimated changes

added theorem NNReal.coe_eq_one
added theorem NNReal.coe_eq_zero
added theorem NNReal.coe_inj
added theorem NNReal.coe_le_coe
added theorem NNReal.coe_le_one
added theorem NNReal.coe_lt_coe
added theorem NNReal.coe_lt_one
added theorem NNReal.coe_mono
added theorem NNReal.coe_ne_one
modified theorem NNReal.coe_ne_zero
added theorem NNReal.coe_one
added theorem NNReal.coe_pos
added theorem NNReal.coe_zero
added theorem NNReal.one_le_coe
added theorem NNReal.one_lt_coe
deleted theorem NNReal.toReal_le_toReal
modified theorem nndist_self