Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ordinal.le_mex_of_forall

Modification history

2023-01-26 09:45
src/set_theory/ordinal/arithmetic.lean
chore(set_theory/game/nim): golf `grundy_value_nim_add_nim` (#15878) …
Added ordinal.le_mex_of_forallView on Github →