Theorem Surreal.mk_le_mk

Modification history

2026-02-20 00:22
Mathlib/SetTheory/Surreal/Basic.lean
chore: remove deprecated material from CGT (#35550) …
Deleted Surreal.mk_le_mkView on Github →
2024-03-09 22:29
Mathlib/SetTheory/Surreal/Basic.lean
feat: Small sets of games/surreals are bounded (#10458) …
Added Surreal.mk_le_mkView on Github →