mathlib3
997fa572 - refactor(set_theory/game/nim): remove `nim` namespace (#15366)

Commit
3 years ago
refactor(set_theory/game/nim): remove `nim` namespace (#15366) A lot of theorems that already had `nim` in the name were also in the `pgame.nim` namespace. We remove the `nim` namespace entirely, and rename the few theorems that didn't have `nim` in the name: - `non_zero_first_wins` → `nim_fuzzy_zero_of_ne_zero` - `add_equiv_zero_iff_eq` → `nim_add_equiv_zero_iff` - `add_fuzzy_zero_iff_ne` → `nim_add_fuzzy_zero_iff` - `equiv_iff_eq` → `nim_equiv_iff_eq` - `grundy_value` → `nim_grundy_value` Further, we move `nim` itself into the `pgame` namespace.
Author
Parents
Loading