Theorem PNat.one_lt_of_lt

Modification history

2026-05-18 15:35
Mathlib/Data/PNat/Basic.lean
feat: `IsBotOneClass ℕ+` (#39056)
Modified PNat.one_lt_of_ltView on Github →
2024-04-28 14:16
Mathlib/Data/PNat/Basic.lean
feat(PNat/Basic): add three lemmas (#12479) …
Added PNat.one_lt_of_ltView on Github →