basic): Golf using `antisymmetrization` API
#13917

Open

feat(set_theory/game/basic): Golf using `antisymmetrization` API #13917

vihdzp wants to merge 11 commits into master from antisymm

add instance

4a4d1564

Merge branch 'master' into preorder

1b9e7a87

tweak

6d05488d

tweak

172fa539

vihdzp added awaiting-review

vihdzp requested a review from

YaelDillies 3 years ago

eric-wieser commented on 2022-05-03

YaelDillies commented on 2022-05-03

Merge branch 'master' into antisymm

688511ff

strengthen instance

aacabfe2

jcommelin requested a review from

YaelDillies 3 years ago

Merge remote-tracking branch 'origin/master' into antisymm

00bdf534

mathlib-dependent-issues-bot added blocked-by-other-PR

mathlib-dependent-issues-bot removed blocked-by-other-PR

Merge branch 'master' into antisymm

cf10a6fc

fix

3c9b4065

YaelDillies removed awaiting-review

YaelDillies added WIP

Merge branch 'master' into antisymm

6975fcbd

Merge branch 'master' into antisymm

0669379d

YaelDillies added awaiting-CI

kim-em added too-late

Reviewers

alreadydone

YaelDillies

eric-wieser

Assignees

No one assigned

Labels

WIP awaiting-CI too-late

Milestone

No milestone

mathlib3 feat(set_theory/game/basic): Golf using `antisymmetrization` API #13917 Open

feat(set_theory/game/basic): Golf using `antisymmetrization` API #13917

mathlib3
feat(set_theory/game/basic): Golf using `antisymmetrization` API
#13917

Open