Skip to content

chore: private many auxiliary results on nimbers#356

Open
vihdzp wants to merge 5 commits intomasterfrom
private
Open

chore: private many auxiliary results on nimbers#356
vihdzp wants to merge 5 commits intomasterfrom
private

Conversation

@vihdzp
Copy link
Copy Markdown
Owner

@vihdzp vihdzp commented Mar 12, 2026

No description provided.

@vihdzp vihdzp added the t-nimber This is mainly about nimbers label Mar 12, 2026
Copy link
Copy Markdown
Contributor

@plp127 plp127 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just a few places where private should be replaced with by exact

Comment thread CombinatorialGames/Nimber/Basic.lean Outdated
Comment thread CombinatorialGames/Nimber/Basic.lean Outdated
Comment thread CombinatorialGames/Nimber/Field.lean Outdated
Comment thread CombinatorialGames/Nimber/Field.lean Outdated
vihdzp and others added 2 commits April 3, 2026 16:18
Co-authored-by: Aaron Liu <aaronliu2008@outlook.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

t-nimber This is mainly about nimbers

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants