Theorem Hyperreal.coe_ofNat

Modification history

2023-12-04 12:41
Mathlib/Data/Real/Hyperreal.lean
fix: add missing `no_index` around `OfNat.ofNat ` (#8317)
Modified Hyperreal.coe_ofNatView on Github →
2023-04-24 22:52
Mathlib/Data/Real/Hyperreal.lean
feat: port Data.Real.Hyperreal (#3586)
Added Hyperreal.coe_ofNatView on Github →