[Merged by Bors] - feat(NumberTheory/Divisors): Define `Nat.divisorsAntidiagonalList` by Paul-Lez · Pull Request #22977 · leanprover-community/mathlib4

Paul-Lez · 2025-03-16T13:27:01Z

This PR defines Nat.divisorsAntidiagonalList and proves a couple of basic results.

This will be used in #21915 (adds a simproc to compute Nat.divisorsAntidiagonal and Int.divisorsAntidiagonal)

github-actions · 2025-03-16T13:28:04Z

PR summary 26fd3e733d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Sorted.filterMap
+ _root_.List.toFinset_filterMap
+ div_lt_div_left
+ div_lt_div_right
+ divisorsAntidiagonalList
+ divisorsAntidiagonalList_one
+ divisorsAntidiagonalList_zero
+ left_le_of_mem_range'
+ lt_iff_lt_of_mul_eq_mul
+ mem_divisorsAntidiagonalList
+ nodup_divisorsAntidiagonalList
+ perm_reverse
+ range'_0
+ reverse_divisorsAntidiagonalList
+ reverse_perm'
+ sorted_divisorsAntidiagonalList_fst
+ sorted_divisorsAntidiagonalList_snd
+ sorted_le_range'
+ sorted_le_replicate
+ sorted_lt_range'
+ sorted_replicate
+ swap_mem_divisorsAntidiagonalList
+ toFinset_divisorsAntidiagonalList
+ toFinset_range'_1
+ toFinset_range'_1_1
+ val_divisorsAntidiagonal
+ ⟨Pairwise.of_reverse,

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).

Mathlib/NumberTheory/Divisors.lean

…lib4 into list-antidiagonal

Mathlib/NumberTheory/Divisors.lean

…lib4 into list-antidiagonal

Mathlib/Data/Finset/Image.lean

Mathlib/Data/List/Sort.lean

Mathlib/Order/Interval/Finset/Nat.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

…munity/mathlib4 into list-antidiagonal

Mathlib/Data/List/Sort.lean

Mathlib/NumberTheory/Divisors.lean

Co-authored-by: Eric Wieser <efw@google.com>

…munity/mathlib4 into list-antidiagonal

eric-wieser

bors d+

Thanks!

I pushed some renames since lemmas about foo.bar should usually be named as if they were Foo.bar foo.

I also pushed a proof_wanted; if you feel like being sniped please try to prove it, but I realize it is totally unhelpful for what you are trying to use this for, so fine to leave it.

mathlib-bors · 2025-04-11T00:18:37Z

✌️ Paul-Lez can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Mathlib/Data/List/Sort.lean

Mathlib/Data/List/Basic.lean

Mathlib/Order/Interval/Finset/Nat.lean

Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>

Paul-Lez · 2025-04-12T12:57:55Z

bors r+

…22977) This PR defines `Nat.divisorsAntidiagonalList` and proves a couple of basic results. This will be used in #21915 (adds a simproc to compute `Nat.divisorsAntidiagonal` and `Int.divisorsAntidiagonal`) Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

mathlib-bors · 2025-04-12T13:51:24Z

Build failed:

Build

Paul-Lez · 2025-04-12T15:38:34Z

bors r+

…22977) This PR defines `Nat.divisorsAntidiagonalList` and proves a couple of basic results. This will be used in #21915 (adds a simproc to compute `Nat.divisorsAntidiagonal` and `Int.divisorsAntidiagonal`) Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

mathlib-bors · 2025-04-12T16:22:32Z

Pull request successfully merged into master.

Build succeeded:

…22977) This PR defines `Nat.divisorsAntidiagonalList` and proves a couple of basic results. This will be used in #21915 (adds a simproc to compute `Nat.divisorsAntidiagonal` and `Int.divisorsAntidiagonal`) Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Init

a963fdf

Paul-Lez added the WIP Work in progress label Mar 16, 2025

b-mehta reviewed Mar 16, 2025

View reviewed changes

Mathlib/NumberTheory/Divisors.lean Outdated Show resolved Hide resolved

Paul-Lez added 4 commits March 16, 2025 15:30

Merge branch 'master' of https://github.com/leanprover-community/math…

8b2ac26

…lib4 into list-antidiagonal

Add doctring

7402027

Move stuff around

7f24d04

Fix namespace issue and lemma variables

826f185

eric-wieser reviewed Mar 17, 2025

View reviewed changes

Mathlib/NumberTheory/Divisors.lean Show resolved Hide resolved

Paul-Lez added 3 commits March 22, 2025 15:49

Add proof that divisorsAntidiagonalList is sorted under the Lex order

b0bf254

Merge branch 'master' of https://github.com/leanprover-community/math…

9be1e31

…lib4 into list-antidiagonal

Move lemmas around

42dabc1

Paul-Lez requested a review from eric-wieser April 3, 2025 21:25

eric-wieser reviewed Apr 3, 2025

View reviewed changes

Mathlib/Data/Finset/Image.lean Outdated Show resolved Hide resolved

Mathlib/Data/List/Sort.lean Outdated Show resolved Hide resolved

Mathlib/Data/List/Sort.lean Outdated Show resolved Hide resolved

Mathlib/Order/Interval/Finset/Nat.lean Outdated Show resolved Hide resolved

Paul-Lez and others added 4 commits April 9, 2025 22:56

Update Mathlib/Data/Finset/Image.lean

5898af4

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Generalize lemma and fix non-terminal simp

a56f5b9

Merge branch 'list-antidiagonal' of https://github.com/leanprover-com…

b116bba

…munity/mathlib4 into list-antidiagonal

Make some variables explicit

431d33e

Paul-Lez requested a review from eric-wieser April 9, 2025 22:00

Fix build error

16a8772

Paul-Lez removed the WIP Work in progress label Apr 9, 2025

Fix other build error

ba74250

eric-wieser reviewed Apr 10, 2025

View reviewed changes

Mathlib/Data/List/Sort.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Apr 10, 2025

View reviewed changes

Mathlib/Data/List/Sort.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Apr 10, 2025

View reviewed changes

Mathlib/NumberTheory/Divisors.lean Outdated Show resolved Hide resolved

Paul-Lez and others added 3 commits April 10, 2025 20:58

Update Mathlib/Data/List/Sort.lean

aa0b4c4

Co-authored-by: Eric Wieser <efw@google.com>

Fix build issue and address review comments

dcf7ef4

Merge branch 'list-antidiagonal' of https://github.com/leanprover-com…

03786b9

…munity/mathlib4 into list-antidiagonal

Paul-Lez requested a review from eric-wieser April 10, 2025 22:14

use cases

16c43aa

whitespace

c2a632e

eric-wieser approved these changes Apr 11, 2025

View reviewed changes

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Apr 11, 2025

b-mehta reviewed Apr 11, 2025

View reviewed changes

YaelDillies and others added 2 commits April 12, 2025 10:48

proof_found

daa19e6

Apply suggestions from code review

33d4562

Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>

Paul-Lez added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 12, 2025

Fix name

a1a18a9

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 12, 2025

Fix lint errors

26fd3e7

Paul-Lez added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 12, 2025

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 12, 2025

mathlib-bors bot changed the title ~~feat(NumberTheory/Divisors): Define Nat.divisorsAntidiagonalList~~ [Merged by Bors] - feat(NumberTheory/Divisors): Define Nat.divisorsAntidiagonalList Apr 12, 2025

mathlib-bors bot closed this Apr 12, 2025

mathlib-bors bot deleted the list-antidiagonal branch April 12, 2025 16:22

Ruben-VandeVelde mentioned this pull request Dec 29, 2025

feat: Rename List.reverse_perm to List.reverse_perm_self and List.reverse_perm' to List.reverse_perm_iff #33276

Open

Conversation

Paul-Lez commented Mar 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Mar 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 26fd3e733d

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Apr 11, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Paul-Lez commented Apr 12, 2025

Uh oh!

mathlib-bors bot commented Apr 12, 2025

Uh oh!

Paul-Lez commented Apr 12, 2025

Uh oh!

mathlib-bors bot commented Apr 12, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Paul-Lez commented Mar 16, 2025 •

edited

Loading

github-actions bot commented Mar 16, 2025 •

edited

Loading