Theorem Ordinal.one_le_iff_pos

Modification history

2024-09-06 22:51

Mathlib/SetTheory/Ordinal/Basic.lean

feat(Algebra/Order/SuccPred): typeclass for `succ x = x + 1` (#16484) …

Deleted Ordinal.one_le_iff_pos View on Github →

2023-02-13 06:43

Mathlib/SetTheory/Ordinal/Basic.lean

feat: port SetTheory.Ordinal.Basic (#2217) …

Added Ordinal.one_le_iff_pos View on Github →