Skip to content

feat: ordinal powers of a field form a basis for nimbers#348

Open
vihdzp wants to merge 13 commits intomasterfrom
addmonoidalg
Open

feat: ordinal powers of a field form a basis for nimbers#348
vihdzp wants to merge 13 commits intomasterfrom
addmonoidalg

Conversation

@vihdzp
Copy link
Copy Markdown
Owner

@vihdzp vihdzp commented Mar 5, 2026

No description provided.

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

plp127 commented Mar 5, 2026

Why do you use AddMonoidAlgebra? You don't need the "algebra" part, right?

@vihdzp
Copy link
Copy Markdown
Owner Author

vihdzp commented Mar 5, 2026

You're right, I've re-stated everything in terms of finsupps.

Comment thread CombinatorialGames/Nimber/Finsupp.lean
Comment thread CombinatorialGames/Nimber/Finsupp.lean
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