feat(NumberTheory/Bernoulli): von Staudt-Clausen theorem by seewoo5 · Pull Request #34906 · leanprover-community/mathlib4

seewoo5 · 2026-02-06T05:55:48Z

Rado's proof ("A New Proof of a Theorem of v. Staudt", JLMS 1935) of von Staudt-Clausen theorem. Initially written by AxiomProver (see commit 97a308e) with further golfs with Claude and Codex.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…n section - Remove unused `Units.val_mk` from simp calls - Convert deprecated `induction'` to `induction` in three lemmas - Fix whitespace: `2*m` → `2 * m`, `2*k` → `2 * k`, `)^(` → `) ^ (` - Fix resulting lines exceeding 100 char limit - Add `set_option linter.style.longFile 1800` for file length Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Simplify several proofs by inlining single-use haves, using pow_succ, removing redundant intermediate steps, and leveraging Finset.sum_filter. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…a proofs Remove `have IH := IH` identity bindings, unwrap redundant `have h1 := ...; exact h1` wrapping, inline single-use omega equalities into pow_succ rewrites, and merge consecutive single-use rewrite steps. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…o callers Merge trivial single-use helper lemmas directly into their sole call sites to reduce declaration count and improve code locality. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Golf 4 verbose proofs by replacing manual have-chains with field_simp/ring, leveraging core_algebraic_identity, and eliminating redundant cast round-trips. Net savings: ~130 lines. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…callers Remove lemmas with 1-2 line proof bodies that are used only once or not at all, inlining their proofs at call sites to reduce indirection. Dead code removed: pIntegral_add, pIntegral_even_term Inlined: geom_sum_of_root_of_unity, generator_pow_card_sub_one_eq_one, pIntegral_neg_pow_div_two, pIntegral_odd_term, power_sum_eq_faulhaber, coprime_add_of_coprime_den, von_staudt_clausen_pos Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…d_rest Replace ~120-line proof with ~15-line proof using by_cases on divisibility, Finset.add_sum_erase for the positive case, and Finset.filter_congr for the negative case. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

github-actions · 2026-02-06T05:57:00Z

PR summary ee3a5404e5

Import changes exceeding 2%

%	File
+25.56%	`Mathlib.NumberTheory.Bernoulli`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.Bernoulli	1639	2058	+419 (+25.56%)

Import changes for all files

Files	Import difference
8 files `Mathlib.NumberTheory.ModularForms.DedekindEta` `Mathlib.NumberTheory.ModularForms.Delta` `Mathlib.NumberTheory.ModularForms.Derivative` `Mathlib.NumberTheory.ModularForms.Discriminant` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion`	8
`Mathlib.NumberTheory.LSeries.HurwitzZetaValues`	80
`Mathlib.NumberTheory.ZetaValues`	81
`Mathlib.NumberTheory.BernoulliPolynomials`	417
`Mathlib.NumberTheory.Bernoulli`	419
`Mathlib.Algebra.BigOperators.Group.Finset.Rat` (new file)	701

Declarations diff

+ bernoulli_add_indicator_eq_sub
+ choose_two_mul_succ_mul_div_eq
+ den_sum_dvd_lcm_den
+ den_sum_dvd_prod_den
+ factorization_succ_le_sub_one
+ faulhaber_sum_div_prime_eq
+ not_dvd_den_bernoulli_add_indicator
+ not_dvd_den_vonStaudt_sum
+ pIntegral
+ pIntegral_bernoulli_even_term
+ pIntegral_choose_mul_pow_div
+ pIntegral_faulhaber_sum
+ pIntegral_mul
+ pIntegral_pow_div
+ prod_one_div_prime_den_coprime
+ sum_one_div_prime_eq_indicator_div_add
+ sum_pow_add_indicator_eq_zero
+ sum_pow_filter_eq_faulhaber
+ vonStaudtIndicator
+ vonStaudtPrimes
+ vonStaudt_clausen

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.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

Add missing documentation for `vonStaudtIndicator` and `pIntegral`. Remove unused arguments from `cast_ne_zero_of_mem_filter`, `generator_pow_ne_one`, `sum_units_pow_eq_zero_of_not_dvd`, `den_pow_div_dvd`, `valuation_bound`, `pIntegral_pow_div_factor`, and `pIntegral_T1`, along with their call sites. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Remove unused arguments from pIntegral_T2, pIntegral_case_one, even_term_decomposition_identity, power_sum_indicator_divisible_by_p, divisibility_to_rat_eq, sum_other_primes_coprime_p_pos, and cascading unused arguments in pIntegral_second_term, pIntegral_coeff_term, pIntegral_first_term, and pIntegral_even_term_in_sum. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…ther Move pIntegral_of_int, pIntegral_mul, pIntegral_mul_int, pIntegral_mul_nat, and pIntegral_sub to directly after pIntegral_sum so all basic pIntegral closure properties are co-located. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Remove pIntegral_nat_mul and use pIntegral_int_mul directly at call sites, relying on Lean's automatic ℕ → ℤ coercion. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Merge the single-use von_staudt_clausen_zero lemma directly into the k = 0 case of von_staudt_clausen. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Remove single-use i1_term_forms_eq and replace it with a shorter `convert` + `push_cast` + `field_simp` proof inside pIntegral_i1_term_in_sum. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Inline ~20 single-use helper lemmas into their callers, reducing the file from ~1053 to 884 lines and from ~80 to 60 definitions. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>

MichaelStollBayreuth · 2026-04-25T19:36:06Z

A general remark: omega should be replaced by lia throughout. (As far as I know, omega is supposed to be phased out, and lia ("linear integer arithmetic", which is part of grind) is the deignated replacement.)

MichaelStollBayreuth · 2026-04-26T19:39:30Z

I think more of the explicit arguments of the private lemmas could be made implicit.

Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>

MichaelStollBayreuth

You could actually move the new lemmas to Mathlib.Algebra.GCDMonoid.FinsetLemmas (and change the title/module docstring of that file to also mention Rat.den or so).

MichaelStollBayreuth · 2026-04-27T09:00:34Z

+
+
+@[expose] public section
+


Suggested change

namespace Rat

MichaelStollBayreuth · 2026-04-27T09:01:12Z

+
+theorem den_sum_dvd_prod_den {ι : Type*} (s : Finset ι) (f : ι → ℚ) :
+    (∑ i ∈ s, f i).den ∣ ∏ i ∈ s, (f i).den :=
+  dvd_trans (den_sum_dvd_lcm_den s f) (s.lcm_dvd_prod (fun i ↦ (f i).den))


Suggested change

dvd_trans (den_sum_dvd_lcm_den s f) (s.lcm_dvd_prod (fun i ↦ (f i).den))

(den_sum_dvd_lcm_den s f).trans <|s.lcm_dvd_prod _

theorem den_prod_dvd_prod_den {ι : Type*} (s : Finset ι) (f : ι → ℚ) :

(∏ i ∈ s, f i).den ∣ ∏ i ∈ s, (f i).den := by

classical

induction s using Finset.induction_on with

| empty => simp

| insert _ _ has ih =>

simp_rw [Finset.prod_insert has]

exact (mul_den_dvd ..).trans <| mul_dvd_mul_left _ ih

end Rat

seewoo5 and others added 14 commits February 5, 2026 15:46

initial vsc

97a308e

style(NumberTheory/Bernoulli): fix lines exceeding 100 char limit

0c0b428

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

style(NumberTheory/Bernoulli): golf proofs in vonStaudtClausen section

231c7e1

Simplify several proofs by inlining single-use haves, using pow_succ, removing redundant intermediate steps, and leveraging Finset.sum_filter. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

style(NumberTheory/Bernoulli): inline 13 single-use helper lemmas int…

2ee2415

…o callers Merge trivial single-use helper lemmas directly into their sole call sites to reduce declaration count and improve code locality. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

style(NumberTheory/Bernoulli): merge and inline consecutive omega haves

6c004ca

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

style(NumberTheory/Bernoulli): remove unused haves and minor cleanup

f0d4ccd

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

minimize imports

8150f9b

revert some claude moves

0bb93d9

wrap lines in sum_primes_eq_indicator_add_rest

65b06cb

github-actions Bot added large-import Automatically added label for PRs with a significant increase in transitive imports t-number-theory Number theory (also use t-algebra or t-analysis to specialize) labels Feb 6, 2026

seewoo5 and others added 9 commits February 5, 2026 22:23

more wrapping

09b4889

minor

4a14bf6

refactor(NumberTheory/Bernoulli): remove pIntegral_nat_mul

a2b5500

Remove pIntegral_nat_mul and use pIntegral_int_mul directly at call sites, relying on Lean's automatic ℕ → ℤ coercion. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

refactor(NumberTheory/Bernoulli): inline von_staudt_clausen_zero

ef90c66

Merge the single-use von_staudt_clausen_zero lemma directly into the k = 0 case of von_staudt_clausen. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

more golf

a6f9018

refactor(NumberTheory/Bernoulli): inline i1_term_forms_eq

19111c7

Remove single-use i1_term_forms_eq and replace it with a shorter `convert` + `push_cast` + `field_simp` proof inside pIntegral_i1_term_in_sum. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

seewoo5 marked this pull request as draft February 6, 2026 17:14

seewoo5 and others added 3 commits February 7, 2026 21:03

remove unused lemmas & add docstring

d46963a

refactor(NumberTheory/Bernoulli): inline single-use lemmas

5d73b9e

Inline ~20 single-use helper lemmas into their callers, reducing the file from ~1053 to 884 lines and from ~80 to 60 definitions. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

small styling

4c210e9

MichaelStollBayreuth reviewed Apr 24, 2026

View reviewed changes

Comment thread Mathlib/NumberTheory/Bernoulli.lean Outdated

MichaelStollBayreuth reviewed Apr 24, 2026

View reviewed changes

Comment thread Mathlib/NumberTheory/Bernoulli.lean Outdated

MichaelStollBayreuth reviewed Apr 24, 2026

View reviewed changes

Comment thread Mathlib/NumberTheory/Bernoulli.lean Outdated

MichaelStollBayreuth reviewed Apr 24, 2026

View reviewed changes

Comment thread Mathlib/NumberTheory/Bernoulli.lean Outdated

MichaelStollBayreuth reviewed Apr 24, 2026

View reviewed changes

Comment thread Mathlib/NumberTheory/Bernoulli.lean Outdated

MichaelStollBayreuth reviewed Apr 24, 2026

View reviewed changes

Comment thread Mathlib/NumberTheory/Bernoulli.lean Outdated

MichaelStollBayreuth reviewed Apr 24, 2026

View reviewed changes

Comment thread Mathlib/NumberTheory/Bernoulli.lean Outdated

MichaelStollBayreuth reviewed Apr 24, 2026

View reviewed changes

Comment thread Mathlib/NumberTheory/Bernoulli.lean Outdated

MichaelStollBayreuth added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 24, 2026

seewoo5 and others added 7 commits April 25, 2026 10:44

Apply suggestions from code review

adb1cc9

Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>

update with suggested proofs & signatures

e61ad45

Change to Ico 1 p

0a0a6ce

inline exists_int_sum_pow_add_indicator_eq

6e31f5b

simplify hfilter

67c7772

Finset is opened

8f3d1bf

minor

66eeda2

MichaelStollBayreuth reviewed Apr 25, 2026

View reviewed changes

Comment thread Mathlib/NumberTheory/Bernoulli.lean Outdated

MichaelStollBayreuth reviewed Apr 25, 2026

View reviewed changes

Comment thread Mathlib/NumberTheory/Bernoulli.lean Outdated

seewoo5 added 3 commits April 25, 2026 13:51

grind

54b8126

inline pIntegral_bernoulli_one_term

f76a91b

one more grind suggestion

360f943

MichaelStollBayreuth reviewed Apr 26, 2026

View reviewed changes

Comment thread Mathlib/NumberTheory/Bernoulli.lean Outdated

seewoo5 and others added 5 commits April 26, 2026 15:20

move den_sum_dvd_prod_den and make some variables implicit

f6719f2

more implicit

d77b828

Update Mathlib/NumberTheory/Bernoulli.lean

6e079d4

Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>

fix implicit

0a9afa3

lake mk_all

a0bf527

MichaelStollBayreuth reviewed Apr 27, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(NumberTheory/Bernoulli): von Staudt-Clausen theorem#34906

feat(NumberTheory/Bernoulli): von Staudt-Clausen theorem#34906
seewoo5 wants to merge 79 commits intoleanprover-community:masterfrom
seewoo5:vsc

seewoo5 commented Feb 6, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Feb 6, 2026 •

edited

Loading

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!

MichaelStollBayreuth commented Apr 25, 2026 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

MichaelStollBayreuth commented Apr 26, 2026

Uh oh!

MichaelStollBayreuth left a comment

Uh oh!

MichaelStollBayreuth Apr 27, 2026

Uh oh!

MichaelStollBayreuth Apr 27, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

-  dvd_trans (den_sum_dvd_lcm_den s f) (s.lcm_dvd_prod (fun i ↦ (f i).den))
+  (den_sum_dvd_lcm_den s f).trans <|s.lcm_dvd_prod _
+theorem den_prod_dvd_prod_den {ι : Type*} (s : Finset ι) (f : ι → ℚ) :
+    (∏ i ∈ s, f i).den ∣ ∏ i ∈ s, (f i).den := by
+  classical
+  induction s using Finset.induction_on with
+  | empty => simp
+  | insert _ _ has ih =>
+    simp_rw [Finset.prod_insert has]
+    exact (mul_den_dvd ..).trans <| mul_dvd_mul_left _ ih
+end Rat

Conversation

seewoo5 commented Feb 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Feb 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary ee3a5404e5

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!

MichaelStollBayreuth commented Apr 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

MichaelStollBayreuth commented Apr 26, 2026

Uh oh!

MichaelStollBayreuth left a comment

Choose a reason for hiding this comment

Uh oh!

MichaelStollBayreuth Apr 27, 2026

Choose a reason for hiding this comment

Uh oh!

MichaelStollBayreuth Apr 27, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

seewoo5 commented Feb 6, 2026 •

edited

Loading

github-actions Bot commented Feb 6, 2026 •

edited

Loading

MichaelStollBayreuth commented Apr 25, 2026 •

edited

Loading