chore(NumberTheory/Zsqrtd): inline duplicated order lemmas into instances#35481
chore(NumberTheory/Zsqrtd): inline duplicated order lemmas into instances#35481FrankieeW wants to merge 11 commits intoleanprover-community:masterfrom
Conversation
github-actions
bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary 965b9674beImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 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 No changes to technical debt.You can run this locally as
|
github-actions
bot
added
the
t-number-theory
There was a problem hiding this comment.
For precisely the reason you give, we should not have this theorem! It should either be made private, or inlined into the linear order instance.
There's a few other theorems in this file like this, such as ZSqrtd.le_total and ZSqrtd.add_le_add_left. Could you fix these too?
Inline `le_antisymm`, `le_total`, `add_le_add_left` into the `LinearOrder`, `Preorder`, and `IsOrderedAddMonoid` instances respectively, and remove the standalone theorems that shadowed root namespace names. Also remove `le_of_add_le_add_left` and `add_lt_add_left` which were only used internally. Update `PellMatiyasevic.lean` to use typeclass `le_antisymm`.
FrankieeW
changed the title
|
Addressed, thanks! I inlined the duplicated order/additive wrapper lemmas into the corresponding instances (including le_total / add_le_add_left / le_antisymm-related wrappers), updated downstream usage to canonical typeclass lemmas, and CI is now green. I also updated the PR title/body to match the final scope. Could you please take another look? |
| | ⟨(_ + 1 : ℕ), -[_+1]⟩ => Nat.le_total _ _ | ||
| | ⟨-[_+1], (_ + 1 : ℕ)⟩ => Nat.le_total _ _ | ||
|
|
||
| protected theorem le_total (a b : ℤ√d) : a ≤ b ∨ b ≤ a := by |
There was a problem hiding this comment.
Could you deprecate these instead of removing them outright? As an example:
@[deprecated (since := "2026-02-19") _root_.le_total]| le_trans a b c hab hbc := by simpa [sub_add_sub_cancel'] using hab.add hbc | ||
| lt_iff_le_not_ge _ _ := (and_iff_right_of_imp (Zsqrtd.le_total _ _).resolve_left).symm | ||
| lt_iff_le_not_ge a b := by | ||
| have ht : b ≤ a ∨ a ≤ b := by |
There was a problem hiding this comment.
This lemma is used twice before the linear order instance is properly built, perhaps that means it should stay but as a private lemma?
| exact (and_iff_right_of_imp ht.resolve_left).symm | ||
|
|
||
| open Int in | ||
| theorem le_arch (a : ℤ√d) : ∃ n : ℕ, a ≤ n := by |
There was a problem hiding this comment.
This seems like a duplicate of exists_nat_ge, which is implied by the Archimedean typeclass.
… lemmas" This reverts commit 9418024.
vihdzp
added
the
awaiting-CI
vihdzp
left a comment
vihdzp
left a comment
There was a problem hiding this comment.
Otherwise LGTM. Thanks for taking care of this, and welcome to Mathlib!
| exact (and_iff_right_of_imp ht.resolve_left).symm | ||
|
|
||
| open Int in | ||
| @[deprecated "Use `exists_nat_ge` where available." (since := "2026-02-19")] |
There was a problem hiding this comment.
I just checked, turns out we don't have an Archimedean instance yet! Can you please leave a TODO for this?
github-actions
bot
removed
the
awaiting-CI
|
Thank you for the review and the helpful guidance! I addressed the requested changes and left a TODO on le_arch noting that an Archimedean (Zsqrtd) instance is not available yet, so callers can migrate to exists_nat_ge once that instance is in place. I will keep watching CI. |
3 participants
This PR follows reviewer feedback by removing duplicated order/additive wrapper theorems in
Zsqrtdand inlining the proofs into the corresponding typeclass instances.Changes include:
Zsqrtd.le_total,Zsqrtd.add_le_add_left,Zsqrtd.le_of_add_le_add_left,Zsqrtd.add_lt_add_left, andZsqrtd.le_antisymmLinearOrder/ ordered additive structure fieldsPellMatiyasevicto the canonical theorem (_root_.le_antisymm)This reduces namespace-level duplicate APIs and keeps proofs aligned with standard typeclass lemmas.