Theorem NNReal.toReal_le_toReal

Modification history

2024-02-12 08:25
Mathlib/Data/Real/NNReal.lean
feat: Complete `NNReal` coercion lemmas (#10214) …
Deleted NNReal.toReal_le_toRealView on Github →
2023-06-12 01:02
Mathlib/Data/Real/NNReal.lean
chore: formatting issues (#4947)
Modified NNReal.toReal_le_toRealView on Github →
2023-06-05 08:37
Mathlib/Data/Real/NNReal.lean
feat: tactic `gcongr` for "relational congruence" (#3965) …
Added NNReal.toReal_le_toRealView on Github →