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

[Merged by Bors] - refactor: make PadicInt.valuation ℕ-valued #19858

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - refactor: make PadicInt.valuation ℕ-valued #19858

wants to merge 1 commit into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Dec 10, 2024 •
edited
Loading

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

Open in Gitpod

@github-actions GitHub Actions
Copy link

github-actions bot commented Dec 10, 2024 •
edited
Loading

PR summary 466f54eb4c

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ valuation_coe
+ valuation_coe_nonneg
+ valuation_inv
+ valuation_zpow
++ le_valuation_add
++ valuation_mul
++ valuation_pow
+++ norm_eq_zpow_neg_valuation
++--- norm_eq_pow_val
- valuation_nonneg

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@YaelDillies YaelDillies added WIP Work in progress t-number-theory Number theory (also use t-algebra or t-analysis to specialize) FLT part of the ongoing formalization of Fermat's Last Theorem labels Dec 10, 2024
@YaelDillies YaelDillies mentioned this pull request Dec 10, 2024
Open
@YaelDillies YaelDillies removed the WIP Work in progress label Dec 10, 2024
loefflerd
loefflerd reviewed Dec 11, 2024
View reviewed changes
Copy link
Collaborator

@loefflerd loefflerd left a comment

Choose a reason for hiding this comment

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

This looks good – thanks for the general cleanup work on the Padics files. Should we also have a version of the valuation taking values in WithTop N, analogous to Padic.addValuation? Anyway, that can be for a later PR.

One question: is there a general reason why it's better not to refer to the Fact section variable by name? I agree we don't usually give explicit names to instance variables, but Fact is obviously a special case, and it loses a few golf points to keep writing (Fact.out : p.Prime) in place of hp.out.

Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean Outdated
Copy link
Collaborator

Choose a reason for hiding this comment

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

These aren't specific to p-adics, so maybe should be split off into a separate mini-PR. What is the rationale for tagging the 1 < a lemmas as simp, but not the 0 < a < 1 lemmas?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I've opened #20032. For the simp tagging, I just followed what was already done in the file

Mathlib/NumberTheory/Padics/PadicIntegers.lean Outdated Show resolved Hide resolved
@loefflerd loefflerd added the awaiting-author A reviewer has asked the author a question or requested changes label Dec 12, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 17, 2024
@YaelDillies YaelDillies force-pushed the padic_int_nat_valuation branch from 18ac305 to 786e002 Compare December 18, 2024 09:39
@YaelDillies YaelDillies removed awaiting-author A reviewer has asked the author a question or requested changes merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Dec 18, 2024
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) labels Dec 18, 2024
@mathlib4-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 20, 2024
@YaelDillies
refactor: make PadicInt.valuation ℕ-valued
466f54e 
It is currently `ℤ`-valued, but always nonnegative.

From FLT
@YaelDillies YaelDillies force-pushed the padic_int_nat_valuation branch from 7076235 to 466f54e Compare December 20, 2024 10:21
@YaelDillies YaelDillies removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 20, 2024
Ruben-VandeVelde
Ruben-VandeVelde approved these changes Dec 20, 2024
View reviewed changes
Copy link
Collaborator

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

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

Thanks!

maintainer merge

@github-actions GitHub Actions
Copy link

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

jcommelin
jcommelin reviewed Dec 21, 2024
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Dec 21, 2024
mathlib-bors bot pushed a commit that referenced this pull request 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
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Dec 21, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title refactor: make PadicInt.valuation ℕ-valued [Merged by Bors] - refactor: make PadicInt.valuation ℕ-valued Dec 21, 2024
@mathlib-bors mathlib-bors bot closed this Dec 21, 2024
@mathlib-bors mathlib-bors bot deleted the padic_int_nat_valuation branch December 21, 2024 08:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin left review comments

@loefflerd loefflerd loefflerd left review comments

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde approved these changes

Assignees
No one assigned
Labels
FLT part of the ongoing formalization of Fermat's Last Theorem maintainer-merge ready-to-merge This PR has been sent to bors. t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

PadicInt.valuation should be ℕ-valued
7 participants
@YaelDillies @mathlib4-dependent-issues-bot @loefflerd @jcommelin @Ruben-VandeVelde @leanprover-community-bot-assistant @leanprover-community-mathlib4-bot