Theorem ENat.natCast_le_of_coe_top_le_withTop

Modification history

2024-11-20 13:28
Mathlib/Data/ENat/Basic.lean
feat: change definition of `HasFTaylorSeries` to take a parameter in `WithTop ℕ∞` instead of `ℕ∞` (#18723) …
Added ENat.natCast_le_of_coe_top_le_withTopView on Github →