Theorem PNat.bit0_le_bit1

Modification history

2024-07-01 15:55

Mathlib/Data/PNat/Basic.lean

chore(Data/PNat): drop `bit*` lemmas (#14217) …

Deleted PNat.bit0_le_bit1 View on Github →

2022-12-23 12:08

Mathlib/Data/PNat/Basic.lean

feat: port Data.PNat.Basic (#1144) …

Added PNat.bit0_le_bit1 View on Github →