Commit 2022-06-19 09:55 5dabef86

feat(set_theory/game/basic): Basic lemmas on inv (#13840) Note that we've redefined inv so that inv x = 0 when x ≈ 0. This is because, in order to lift it to an operation on surreals, we need to prove that equivalent numeric games give equivalent numeric values, and this isn't the case otherwise.