feat: birthday of `Dyadic.toIGame x` - #428

Merged

vihdzp merged 28 commits into

vihdzp:masterfrom

plp127:aliu/birthday-dyadic

Sep 12, 2026

Commits on Aug 5, 2026

prove theorem
plp127
committed
2b099c6
prove more theorem
plp127
committed
cb1a552

Commits on Aug 6, 2026

Merge branch 'aliu/birthday_intCast' into aliu/birthday-dyadic
plp127
committed
b33aef5
prove theorem
plp127
committed
ac2a208
add docstring
plp127
committed
fb380a5
Merge branch 'master' into aliu/birthday-dyadic
plp127
committed
c35f9f6
add lemmas and examples
plp127
committed
504ff05

Commits on Aug 13, 2026

Update CombinatorialGames/Surreal/Birthday/Dyadic.lean

plp127
and
vihdzp
authored
14193c0
Apply suggestions from code review

plp127
and
vihdzp
authored
6db4bee
write new dyadic lemmas
plp127
committed
fdf2d56
fix changes
plp127
committed
63fbf31
Update CombinatorialGames/Surreal/Birthday/Dyadic.lean

plp127
and
vihdzp
authored
d2c92e1

Commits on Aug 14, 2026

split proof
plp127
committed
e3f6285

Commits on Aug 20, 2026

add PR guard
plp127
committed
10b4825

Commits on Sep 12, 2026

Update CombinatorialGames/Surreal/Birthday/Dyadic.lean

plp127
and
vihdzp
authored
43a91fa
Apply batched suggestions from code review

plp127
and
vihdzp
authored
ab6188a
add result to docstring
plp127
committed
9bd4fac
Apply batched suggestions from code review

plp127
and
vihdzp
authored
73365b2
Apply batched suggestions from code review

plp127
and
vihdzp
authored
f86f1a4
Apply suggestion from @vihdzp

plp127
and
vihdzp
authored
65efaab
empty lines
plp127
committed
8999c69
fix line endings (CRLF -> LF)
plp127
committed
c4e66f6
make `@[simp]`
plp127
committed
8da3034
use `subst`
plp127
committed
4955f5c
use `contrapose`
plp127
committed
8635ae8
reduce mouthful
plp127
committed
921ba73
Merge branch 'master' into aliu/birthday-dyadic
plp127
committed
df061dc
fix build
plp127
committed
7478ffa