feat: reverse all options of a game - #430

Open

plp127 wants to merge 15 commits into

vihdzp:masterfrom

plp127:aliu/canonical

Commits on Aug 11, 2026

start unreversing
plp127
committed
9126075
fix definition
plp127
committed
493953a
prove theorem
plp127
committed
cbad2ec
prove another theorem
plp127
committed
b648b70
prove more theorem
plp127
committed
cff6196
prove main theorem
plp127
committed
37c8e3c
unpublic stuff
plp127
committed
52d5d9f
add docstring
plp127
committed
51aaf69

Commits on Aug 12, 2026

add docstrings
plp127
committed
10c5954

Commits on Aug 13, 2026

add unfolding lemmas
plp127
committed
701883b
Update CombinatorialGames/Game/Canonical.lean

plp127
and
vihdzp
authored
a1eaa65
make implicit
plp127
committed
7ef2a84
make public
plp127
committed
24774b4
prove idem theorem
plp127
committed
a634aa2

Commits on Aug 14, 2026

add lemma
plp127
committed
ded06b8