Skip to content

[Merged by Bors] - feat: telescopic product/sum over Fin#36674

Closed
EtienneC30 wants to merge 14 commits intoleanprover-community:masterfrom
EtienneC30:telescope
Closed

[Merged by Bors] - feat: telescopic product/sum over Fin#36674
EtienneC30 wants to merge 14 commits intoleanprover-community:masterfrom
EtienneC30:telescope

Conversation

@EtienneC30
Copy link
Copy Markdown
Member

@EtienneC30 EtienneC30 commented Mar 15, 2026

Open in Gitpod

@EtienneC30 EtienneC30 added the t-algebra Algebra (groups, rings, fields, etc) label Mar 15, 2026
@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Mar 15, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 15, 2026 •
edited
Loading

PR summary 60ed60fabc

Import changes exceeding 2%

% File
+2.89% Mathlib.Algebra.BigOperators.Intervals

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Algebra.BigOperators.Intervals 622 640 +18 (+2.89%)
Mathlib.Combinatorics.SetFamily.AhlswedeZhang 799 814 +15 (+1.88%)
Import changes for all files
Files Import difference
Mathlib.NumberTheory.Multiplicity 6
10 files Mathlib.Algebra.CharP.Frobenius Mathlib.Algebra.CharP.Lemmas Mathlib.Algebra.CharP.Reduced Mathlib.Data.Nat.Choose.Factorization Mathlib.Data.Nat.Multiplicity Mathlib.Data.Nat.Squarefree Mathlib.NumberTheory.MaricaSchoenheim Mathlib.NumberTheory.Padics.PadicNorm Mathlib.NumberTheory.Padics.PadicVal.Basic Mathlib.NumberTheory.SmoothNumbers
 7
Mathlib.NumberTheory.Basic Mathlib.RingTheory.Ideal.Basic 12
Mathlib.Algebra.Order.CauSeq.BigOperators 14
15 files Mathlib.Algebra.Field.GeomSum Mathlib.Algebra.Order.Field.GeomSum Mathlib.Algebra.Order.Ring.GeomSum Mathlib.Algebra.Order.Ring.IsNonarchimedean Mathlib.Algebra.Ring.Divisibility.Lemmas Mathlib.Algebra.Ring.GeomSum Mathlib.Algebra.Squarefree.Basic Mathlib.Combinatorics.Colex Mathlib.Combinatorics.SetFamily.AhlswedeZhang Mathlib.Combinatorics.SetFamily.KruskalKatona Mathlib.Data.Nat.Choose.Sum Mathlib.NumberTheory.FactorisationProperties Mathlib.NumberTheory.Primorial Mathlib.RingTheory.Nilpotent.Basic Mathlib.RingTheory.Radical.Basic
 15
5 files Mathlib.Algebra.BigOperators.Intervals Mathlib.Algebra.BigOperators.Module Mathlib.Data.Nat.Digits.Div Mathlib.Data.Nat.Digits.Lemmas Mathlib.Data.Nat.Factorial.SuperFactorial
 18

Declarations diff

+ Fin.prod_Icc_div
+ Fin.prod_Iic_div
+ Finset.prod_fin_Icc_eq_prod_nat_Icc
+ prod_Icc_div

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

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

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

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

@github-actions github-actions bot added the t-data Data (lists, quotients, numbers, etc) label Mar 15, 2026
eric-wieser
eric-wieser reviewed Mar 15, 2026
View reviewed changes
@EtienneC30 EtienneC30 mentioned this pull request Mar 17, 2026
Open
2 tasks
joneugster
joneugster reviewed Mar 27, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@joneugster joneugster left a comment

Choose a reason for hiding this comment

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

Overall the PR looks good to me, thanks! See comment about simp-set

@joneugster joneugster added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 27, 2026
@EtienneC30 EtienneC30 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 29, 2026
@EtienneC30
Copy link
Copy Markdown
Member Author

EtienneC30 commented Mar 29, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 29, 2026 •
edited
Loading

Benchmark results for 38ca5c2 against 60ed60f are in. There are no significant changes. @EtienneC30

  • ✅ build//instructions: -56.7G (-0.03%)

Small changes (1🟥)

  • 🟥 build/module/Mathlib.Algebra.BigOperators.Intervals//instructions: +7.1G (+48.88%)

@joneugster
Copy link
Copy Markdown
Contributor

joneugster commented Mar 29, 2026

Thanks!

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 29, 2026

🚀 Pull request has been placed on the maintainer queue by joneugster.

issue_comment, wf_run

@mathlib-triage mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Mar 29, 2026
riccardobrasca
riccardobrasca reviewed Mar 30, 2026
View reviewed changes
Copy link
Copy Markdown
Member

@riccardobrasca riccardobrasca 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

mathlib-bors bot pushed a commit that referenced this pull request Mar 30, 2026
@EtienneC30
feat: telescopic product/sum over Fin (#36674)
54ac04e
@mathlib-triage mathlib-triage bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Mar 30, 2026
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 30, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: telescopic product/sum over Fin [Merged by Bors] - feat: telescopic product/sum over Fin Mar 30, 2026
@mathlib-bors mathlib-bors bot closed this Mar 30, 2026
aditya-ramabadran pushed a commit to aditya-ramabadran/mathlib4 that referenced this pull request Apr 1, 2026
@EtienneC30 @aditya-ramabadran
feat: telescopic product/sum over Fin (leanprover-community#36674)
0900da2
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@joneugster joneugster joneugster left review comments

@riccardobrasca riccardobrasca riccardobrasca left review comments

Assignees

@joneugster joneugster

Labels

large-import Automatically added label for PRs with a significant increase in transitive imports ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc) t-data Data (lists, quotients, numbers, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@EtienneC30 @leanprover-radar @joneugster @eric-wieser @riccardobrasca