Commit 2024-07-14 01:52 cdb5bd69

View on Github →

feat(SetTheory/Surreal/Basic): add some lemmas for Surreal.mk (#14600) add some lemmas for Surreal.mk

Estimated changes

added theorem Surreal.mk_add
added theorem Surreal.mk_eq_mk
added theorem Surreal.mk_eq_zero
added theorem Surreal.mk_lt_mk
added theorem Surreal.mk_sub
added theorem Surreal.zero_def
added theorem Surreal.zero_le_mk
added theorem Surreal.zero_lt_mk