Commit 2021-04-18 14:42 3953378b
View on Github →feat(set_theory/surreal): add add_monoid instance (#7228) This PR is a part of a project for putting ordered abelian group structure on surreal numbers. Zulip We construct add_monoid instance for surreal numbers. The "term_type" proofs suggested on the above Zulip thread are not working nicely as Lean is unable to infer the type of the setoid.