Theorem Real.toNNReal_coe_nat

Modification history

2025-03-12 23:13
Mathlib/Data/NNReal/Defs.lean
chore(Data/(E)(NN)Real): address porting notes (#22883) …
Added Real.toNNReal_coe_natView on Github →