Theorem EReal.natCast_mul

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.natCast_mulView on Github →