Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

PadicInt.valuation should be ℕ-valued #277

Open
YaelDillies opened this issue Dec 9, 2024 · 5 comments
Open

PadicInt.valuation should be ℕ-valued #277

YaelDillies opened this issue Dec 9, 2024 · 5 comments
Assignees
@YaelDillies

Comments

@YaelDillies
Copy link
Contributor

PadicInt.valuation is currently ℤ-valued, but only takes nonnegative values.
@YaelDillies
Copy link
Contributor Author

claim

@github-actions GitHub Actions
Copy link
Contributor

github-actions bot commented Dec 9, 2024

This issue cannot be assigned to @YaelDillies because it has not been added to the project board by the project maintainers.

Please consider discussing the issue on our Zulip channel. To understand the contribution process, please read the CONTRIBUTING guide.

@kbuzzard
Copy link
Collaborator

You should be able to claim it now @YaelDillies

@github-project-automation github-project-automation bot moved this to Unclaimed in FLT Project Dec 10, 2024
@YaelDillies
Copy link
Contributor Author

claim

@kbuzzard kbuzzard moved this from Unclaimed to Claimed in FLT Project Dec 10, 2024
@YaelDillies YaelDillies mentioned this issue Dec 10, 2024
Closed
1 task
@YaelDillies
Copy link
Contributor Author

propose leanprover-community/mathlib4#19858

mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this issue Dec 21, 2024
@YaelDillies
refactor: make PadicInt.valuation ℕ-valued (#19858)
1c080cc 
It is currently `ℤ`-valued, but always nonnegative.

Also rename the misnamed `norm_eq_pow_val` to `norm_eq_zpow_neg_valuation`

From FLT

Closes ImperialCollegeLondon/FLT#277
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@YaelDillies YaelDillies

Labels
None yet
Projects
FLT Project
Status: Claimed
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

[Merged by Bors] - refactor: make PadicInt.valuation ℕ-valued leanprover-community/mathlib4
2 participants
@YaelDillies @kbuzzard