Theorem Surreal.mk_eq_mk

Modification history

2026-02-20 00:22
Mathlib/SetTheory/Surreal/Basic.lean
chore: remove deprecated material from CGT (#35550) …
Deleted Surreal.mk_eq_mkView on Github →
2024-07-14 01:52
Mathlib/SetTheory/Surreal/Basic.lean
feat(SetTheory/Surreal/Basic): add some lemmas for Surreal.mk (#14600) …
Added Surreal.mk_eq_mkView on Github →