Theorem PNat.mk_lt_mk

Modification history

2025-03-14 05:54

Mathlib/Data/PNat/Defs.lean

chore(Data): go through remaining porting notes (#22907) …

Modified PNat.mk_lt_mk View on Github →

2022-11-17 12:36

Mathlib/Data/PNat/Defs.lean

feat: port Data.PNat.Defs (#604) …

Added PNat.mk_lt_mk View on Github →