Theorem PartENat.ofNat_lt_top

Modification history

2025-01-07 09:21

Mathlib/Data/Nat/PartENat.lean

chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521) …

Modified PartENat.ofNat_lt_top View on Github →

2023-11-08 15:51

Mathlib/Data/Nat/PartENat.lean

chore(PartENat): golf and improve `ofNat` support (#8002) …

Added PartENat.ofNat_lt_top View on Github →