Theorem PartENat.ofENat_ofNat

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

2024-03-24 09:49

Mathlib/Data/Nat/PartENat.lean

fix: improve simp lemmas around PartENat.ofENat (#11553)

Added PartENat.ofENat_ofNat View on Github →