Theorem EReal.coe_coe_eq_natCast

Modification history

2024-07-18 16:46
Mathlib/Data/Real/EReal.lean
feat(Data.Real.ENatENNReal/EReal): add a few coe lemmas (#14835) …
Added EReal.coe_coe_eq_natCastView on Github →