Theorem PartENat.withTopEquiv_symm_one

Modification history

2024-03-24 09:49

Mathlib/Data/Nat/PartENat.lean

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

Modified PartENat.withTopEquiv_symm_one View on Github →

2023-11-08 15:51

Mathlib/Data/Nat/PartENat.lean

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

Added PartENat.withTopEquiv_symm_one View on Github →