Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
seewoo5 wants to merge 57 commits into
base: master
Choose a base branch
from
+384 −4
Open

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

Show file tree
Hide file tree
Changes from 33 commits
Commits
Show all changes
57 commits
Select commit Hold shift + click to select a range
97a308e
initial vsc
seewoo5 Feb 5, 2026
0c0b428
style(NumberTheory/Bernoulli): fix lines exceeding 100 char limit
seewoo5 Feb 6, 2026
80fd768
style(NumberTheory/Bernoulli): fix linter warnings in vonStaudtClause…
seewoo5 Feb 6, 2026
231c7e1
style(NumberTheory/Bernoulli): golf proofs in vonStaudtClausen section
seewoo5 Feb 6, 2026
cead7cd
style(NumberTheory/Bernoulli): remove redundant haves and inline omeg…
seewoo5 Feb 6, 2026
2ee2415
style(NumberTheory/Bernoulli): inline 13 single-use helper lemmas int…
seewoo5 Feb 6, 2026
b8c3f4b
style(NumberTheory/Bernoulli): golf long proofs with field_simp/ring
seewoo5 Feb 6, 2026
df32f12
style(NumberTheory/Bernoulli): inline 9 single-use short lemmas into …
seewoo5 Feb 6, 2026
6c004ca
style(NumberTheory/Bernoulli): merge and inline consecutive omega haves
seewoo5 Feb 6, 2026
f0d4ccd
style(NumberTheory/Bernoulli): remove unused haves and minor cleanup
seewoo5 Feb 6, 2026
8150f9b
minimize imports
seewoo5 Feb 6, 2026
0bb93d9
revert some claude moves
seewoo5 Feb 6, 2026
65b06cb
wrap lines in sum_primes_eq_indicator_add_rest
seewoo5 Feb 6, 2026
1d9df81
refactor(NumberTheory/Bernoulli): simplify sum_primes_eq_indicator_ad…
seewoo5 Feb 6, 2026
56384d4
fix(NumberTheory/Bernoulli): add docstrings and remove unused arguments
seewoo5 Feb 6, 2026
7442b70
fix(NumberTheory/Bernoulli): remove remaining unused arguments
seewoo5 Feb 6, 2026
09b4889
more wrapping
seewoo5 Feb 6, 2026
b708270
refactor(NumberTheory/Bernoulli): group pIntegral closure lemmas toge…
seewoo5 Feb 6, 2026
4a14bf6
minor
seewoo5 Feb 6, 2026
a2b5500
refactor(NumberTheory/Bernoulli): remove pIntegral_nat_mul
seewoo5 Feb 6, 2026
ef90c66
refactor(NumberTheory/Bernoulli): inline von_staudt_clausen_zero
seewoo5 Feb 6, 2026
a6f9018
more golf
seewoo5 Feb 6, 2026
19111c7
refactor(NumberTheory/Bernoulli): inline i1_term_forms_eq
seewoo5 Feb 6, 2026
d46963a
remove unused lemmas & add docstring
seewoo5 Feb 8, 2026
5d73b9e
refactor(NumberTheory/Bernoulli): inline single-use lemmas
seewoo5 Feb 8, 2026
4c210e9
small styling
seewoo5 Feb 8, 2026
3e07cbd
refactor(NumberTheory/Bernoulli): use FiniteField.sum_pow_units for p…
seewoo5 Feb 8, 2026
3a620bc
refactor: inline core_algebraic_identity in Bernoulli proof
seewoo5 Feb 14, 2026
114ff9f
docs: add Rado-proof docstrings in Bernoulli
seewoo5 Feb 14, 2026
d5377ba
add reference and author
seewoo5 Feb 14, 2026
f21dbe6
refactor: golf pIntegral and range-sum steps in Bernoulli
seewoo5 Feb 14, 2026
49d2886
refactor: simplify cast transport in bernoulli rearrangement
seewoo5 Feb 14, 2026
592a222
Merge branch 'master' into vsc
seewoo5 Feb 14, 2026
f32268b
article -> Article
seewoo5 Feb 14, 2026
f5674aa
Update Mathlib/NumberTheory/Bernoulli.lean
seewoo5 Feb 22, 2026
42d5228
Merge branch 'master' into vsc
seewoo5 Feb 26, 2026
b03fd7d
Merge branch 'master' into vsc
seewoo5 Mar 4, 2026
6717d2f
Merge branch 'master' into vsc
seewoo5 Mar 9, 2026
7f148f4
Apply suggestions from code review
seewoo5 Mar 9, 2026
dc3d034
Merge branch 'vsc' of github.com:seewoo5/mathlib4 into vsc
seewoo5 Mar 9, 2026
0e36861
change function notations
seewoo5 Mar 9, 2026
b8d57fe
change definition of pIntegral using padicValuation
seewoo5 Mar 10, 2026
2b3fbbb
use lia and golf pIntegral lemma proofs
seewoo5 Mar 10, 2026
c9e5e09
renaming
seewoo5 Mar 10, 2026
6a54439
better renaming?
seewoo5 Mar 10, 2026
ac94b94
minor
seewoo5 Mar 11, 2026
e6b68c4
Merge branch 'master' into vsc
seewoo5 Mar 19, 2026
b75cb0a
wip
seewoo5 Mar 21, 2026
b8b0f48
Merge branch 'master' into vsc
seewoo5 Apr 7, 2026
db3cd33
refactor: inline single-use helper lemmas in von Staudt-Clausen proof
seewoo5 Apr 7, 2026
9462b04
refactor: shorten verbose proofs in von Staudt-Clausen
seewoo5 Apr 7, 2026
2e45cb0
refactor: use shorter tactics in von Staudt-Clausen proof
seewoo5 Apr 7, 2026
9a99e15
refactor: shorten pIntegral_bernoulli_one_term and pIntegral_bernoull…
seewoo5 Apr 7, 2026
fc7e1eb
style: remove redundant type casts in von Staudt-Clausen proof
seewoo5 Apr 7, 2026
83e6593
refactor: use fewer, more powerful tactics in von Staudt-Clausen proof
seewoo5 Apr 7, 2026
7f53e32
more golfs
seewoo5 Apr 16, 2026
a6d2933
Merge branch 'master' into vsc
seewoo5 Apr 16, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Loading
Loading