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

Open

seewoo5 wants to merge 64 commits intoleanprover-community:masterfrom

Commits on Feb 5, 2026

initial vsc
seewoo5
committed

Commits on Feb 6, 2026

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

seewoo5
and
claude
committed
style(NumberTheory/Bernoulli): fix linter warnings in vonStaudtClausen section

seewoo5
and
claude
committed
style(NumberTheory/Bernoulli): golf proofs in vonStaudtClausen section

seewoo5
and
claude
committed
style(NumberTheory/Bernoulli): remove redundant haves and inline omega proofs

seewoo5
and
claude
committed
style(NumberTheory/Bernoulli): inline 13 single-use helper lemmas into callers

seewoo5
and
claude
committed
style(NumberTheory/Bernoulli): golf long proofs with field_simp/ring

seewoo5
and
claude
committed
style(NumberTheory/Bernoulli): inline 9 single-use short lemmas into callers

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

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

seewoo5
and
claude
committed
minimize imports
seewoo5
committed
revert some claude moves
seewoo5
committed
wrap lines in sum_primes_eq_indicator_add_rest
seewoo5
committed
refactor(NumberTheory/Bernoulli): simplify sum_primes_eq_indicator_add_rest

seewoo5
and
claude
committed
fix(NumberTheory/Bernoulli): add docstrings and remove unused arguments

seewoo5
and
claude
committed
fix(NumberTheory/Bernoulli): remove remaining unused arguments

seewoo5
and
claude
committed
more wrapping
seewoo5
committed
refactor(NumberTheory/Bernoulli): group pIntegral closure lemmas together

seewoo5
and
claude
committed
minor
seewoo5
committed
refactor(NumberTheory/Bernoulli): remove pIntegral_nat_mul

seewoo5
and
claude
committed
refactor(NumberTheory/Bernoulli): inline von_staudt_clausen_zero

seewoo5
and
claude
committed
more golf
seewoo5
committed
refactor(NumberTheory/Bernoulli): inline i1_term_forms_eq

seewoo5
and
claude
committed

Commits on Feb 22, 2026

Update Mathlib/NumberTheory/Bernoulli.lean

seewoo5
and
kckennylau
authored

Commits on Feb 26, 2026

Merge branch 'master' into vsc
seewoo5
committed

Commits on Mar 4, 2026

Merge branch 'master' into vsc
seewoo5
authored

Commits on Mar 10, 2026

Commits on Mar 11, 2026

minor
seewoo5
committed

Commits on Mar 19, 2026

Merge branch 'master' into vsc
seewoo5
committed

Commits on Mar 21, 2026

wip
seewoo5
committed

Commits on Apr 7, 2026

Commits on Apr 16, 2026