Theorem ENat.toENNReal_coe_eq_iff

Modification history

2024-12-30 10:07
Mathlib/Data/Real/ENatENNReal.lean
chore: Rename injectivity theorems for consistency (#20329) …
Deleted ENat.toENNReal_coe_eq_iffView on Github →
2024-07-18 16:46
Mathlib/Data/Real/ENatENNReal.lean
feat(Data.Real.ENatENNReal/EReal): add a few coe lemmas (#14835) …
Added ENat.toENNReal_coe_eq_iffView on Github →