Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-09 18:57 b8fb8e5b

View on Github →

feat(set_theory/ordinal_arithmetic): le_one_iff (#11847)

Estimated changes

added theorem ordinal.le_one_iff