[Merged by Bors] - feat: finset of pairs of divisors of an integer#21912
Closed
YaelDillies wants to merge 3 commits intomasterfrom
Closed
[Merged by Bors] - feat: finset of pairs of divisors of an integer#21912YaelDillies wants to merge 3 commits intomasterfrom
YaelDillies wants to merge 3 commits intomasterfrom
Conversation
PR summary 2b103c0419
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.NumberTheory.Divisors | 628 | 639 | +11 (+1.75%) |
Import changes for all files
| Files | Import difference |
|---|---|
66 filesMathlib.Algebra.Algebra.ZMod Mathlib.Algebra.CharP.CharAndCard Mathlib.Algebra.CharP.Two Mathlib.Algebra.Field.NegOnePow Mathlib.Algebra.Field.ZMod Mathlib.Algebra.Homology.BifunctorAssociator Mathlib.Algebra.Homology.BifunctorFlip Mathlib.Algebra.Homology.Bifunctor Mathlib.Algebra.Homology.ComplexShapeSigns Mathlib.Algebra.Homology.Monoidal Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Algebra.Homology.TotalComplex Mathlib.Algebra.Order.Antidiag.Nat Mathlib.Algebra.Order.Chebyshev Mathlib.Algebra.Ring.NegOnePow Mathlib.Algebra.Ring.Periodic Mathlib.CategoryTheory.Triangulated.Functor Mathlib.CategoryTheory.Triangulated.Pretriangulated Mathlib.CategoryTheory.Triangulated.TStructure.Basic Mathlib.CategoryTheory.Triangulated.TriangleShift Mathlib.CategoryTheory.Triangulated.Triangulated Mathlib.Combinatorics.SimpleGraph.DegreeSum Mathlib.Combinatorics.SimpleGraph.Matching Mathlib.Combinatorics.SimpleGraph.UniversalVerts Mathlib.Data.Finset.NatDivisors Mathlib.Data.Nat.Factorization.PrimePow Mathlib.Data.Nat.Periodic Mathlib.Data.Nat.Squarefree Mathlib.Data.Nat.Totient Mathlib.Data.ZMod.Aut Mathlib.Data.ZMod.Basic Mathlib.Data.ZMod.Factorial Mathlib.Data.ZMod.IntUnitsPower Mathlib.Data.ZMod.Units Mathlib.Data.ZMod.ValMinAbs Mathlib.GroupTheory.CommutingProbability Mathlib.GroupTheory.Exponent Mathlib.GroupTheory.FixedPointFree Mathlib.GroupTheory.GroupAction.Period Mathlib.GroupTheory.NoncommPiCoprod Mathlib.GroupTheory.OrderOfElement Mathlib.GroupTheory.Perm.Centralizer Mathlib.GroupTheory.Perm.Closure Mathlib.GroupTheory.Perm.ConjAct Mathlib.GroupTheory.Perm.Cycle.Basic Mathlib.GroupTheory.Perm.Cycle.Concrete Mathlib.GroupTheory.Perm.Cycle.Factors Mathlib.GroupTheory.Perm.Cycle.PossibleTypes Mathlib.GroupTheory.Perm.Cycle.Type Mathlib.GroupTheory.Perm.Fin Mathlib.GroupTheory.Perm.Finite Mathlib.GroupTheory.SpecificGroups.Dihedral Mathlib.LinearAlgebra.FiniteSpan Mathlib.NumberTheory.ArithmeticFunction Mathlib.NumberTheory.DirichletCharacter.Basic Mathlib.NumberTheory.FactorisationProperties Mathlib.NumberTheory.LegendreSymbol.ZModChar Mathlib.NumberTheory.LucasLehmer Mathlib.NumberTheory.MaricaSchoenheim Mathlib.NumberTheory.MulChar.Basic Mathlib.NumberTheory.Padics.PadicNorm Mathlib.NumberTheory.Padics.PadicVal.Basic Mathlib.NumberTheory.PrimeCounting Mathlib.NumberTheory.SmoothNumbers Mathlib.RingTheory.Fintype Mathlib.SetTheory.Nimber.Field |
1 |
Mathlib.NumberTheory.Divisors |
11 |
Declarations diff
+ cast_eq_neg_cast
+ divisorsAntidiag
+ divisorsAntidiag_natCast
+ divisorsAntidiag_neg
+ divisorsAntidiag_neg_natCast
+ divisorsAntidiag_ofNat
+ divisorsAntidiag_zero
+ map_neg_divisorsAntidiag
+ map_prodComm_divisorsAntidiag
+ mem_divisorsAntidiag
+ neg_cast_eq_cast
+ neg_mem_divisorsAntidiag
+ swap_mem_divisorsAntidiag
++ prodMk_mem_divisorsAntidiag
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
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
eric-wieser
reviewed
Feb 15, 2025
| `n.divisorsAntidiagonal` is the finset of pairs `(a, b) : ℕ × ℕ` such that `a * b = n`. | ||
| As a special case, `Nat.divisorsAntidiagonal 0 = ∅`. | ||
|
|
||
| O(n). -/ |
Member
There was a problem hiding this comment.
I put it to you that "$O(n)$." is not a full sentence.
Contributor
Author
There was a problem hiding this comment.
I am following the convention established by https://leanprover-community.github.io/mathlib4_docs/Init/Data/List/Basic.html#List.range
eric-wieser
reviewed
Feb 15, 2025
eric-wieser
reviewed
Feb 15, 2025
eric-wieser
reviewed
Feb 15, 2025
eric-wieser
reviewed
Feb 15, 2025
2 tasks
eric-wieser
reviewed
Feb 15, 2025
eric-wieser
reviewed
Feb 15, 2025
eric-wieser
reviewed
Feb 15, 2025
eric-wieser
reviewed
Feb 15, 2025
eric-wieser
reviewed
Feb 15, 2025
Member
eric-wieser
left a comment
There was a problem hiding this comment.
Some more (simp) lemma ideas:
divisorsAntidiag (-z) = (divisorsAntidiag z).map _divisorsAntidiag (ofNat(n)) = disjUnion (Nat.divisorsAntidiag n).map ...
7011fbe to
becfceb
Compare
Compute the antidiagonal of divisors of an integer `z`, namely the finset of pairs `(a, b) : ℤ × ℤ` such that `a * b = n` (unless `z = 0`, in which case we set the finset to be empty by convention).
becfceb to
c46905b
Compare
Collaborator
|
This PR/issue depends on: |
j-loreaux
reviewed
Feb 16, 2025
Contributor
j-loreaux
left a comment
There was a problem hiding this comment.
LGTM otherwise!
bors d+
Contributor
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
eric-wieser
reviewed
Feb 16, 2025
Contributor
Author
|
bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Feb 17, 2025
Compute the antidiagonal of divisors of an integer `z`, namely the finset of pairs `(a, b) : ℤ × ℤ` such that `a * b = n` (unless `z = 0`, in which case we set the finset to be empty by convention).
Contributor
Author
|
Sorry, forgot to push bors r- |
Contributor
|
Canceled. |
Contributor
Author
|
bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Feb 17, 2025
Compute the antidiagonal of divisors of an integer `z`, namely the finset of pairs `(a, b) : ℤ × ℤ` such that `a * b = n` (unless `z = 0`, in which case we set the finset to be empty by convention).
Contributor
|
Pull request successfully merged into master. Build succeeded: |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Compute the antidiagonal of divisors of an integer
z, namely the finset of pairs(a, b) : ℤ × ℤsuch thata * b = n(unlessz = 0, in which case we set the finset to be empty by convention).RingandFieldparts #21920