Skip to content

Split over-long proofs in AndersonConjecture #756

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

Merged
Vilin97 merged 4 commits into from
Nov 5, 2026
Merged

Split over-long proofs in AndersonConjecture #756

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
1821a80
Split over-long proofs in AndersonConjecture
Vilin97 Nov 5, 2026
3ebef2a
Remove the now-unused smul_lift_of_filtration
Vilin97 Nov 5, 2026
ad05935
Preserve the public filtration lifting lemma
Vilin97 Nov 5, 2026
4b1e37f
Put theorem headers on their own line after include/omit
Vilin97 Nov 5, 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
595 changes: 259 additions & 336 deletions LeanPool/AndersonConjecture/AdicNoetherian.lean
View file
Open in desktop

Large diffs are not rendered by default.

428 changes: 222 additions & 206 deletions LeanPool/AndersonConjecture/Jensen/Adjoin/Adjoin.lean
View file
Open in desktop

Large diffs are not rendered by default.

427 changes: 224 additions & 203 deletions LeanPool/AndersonConjecture/Jensen/Adjoin/FromPrime.lean
View file
Open in desktop

Large diffs are not rendered by default.

826 changes: 422 additions & 404 deletions LeanPool/AndersonConjecture/Jensen/CloseUp/AvoidanceStep.lean
View file
Open in desktop

Large diffs are not rendered by default.

401 changes: 204 additions & 197 deletions LeanPool/AndersonConjecture/Jensen/CloseUp/CoprimeSplit.lean
View file
Open in desktop

Large diffs are not rendered by default.

425 changes: 204 additions & 221 deletions LeanPool/AndersonConjecture/Jensen/CloseUp/Factor.lean
View file
Open in desktop

Large diffs are not rendered by default.

884 changes: 438 additions & 446 deletions LeanPool/AndersonConjecture/Jensen/CloseUp/NoCommonFactor.lean
View file
Open in desktop

Large diffs are not rendered by default.

220 changes: 124 additions & 96 deletions LeanPool/AndersonConjecture/Jensen/CombinedStep.lean
View file
Open in desktop

Large diffs are not rendered by default.

594 changes: 289 additions & 305 deletions LeanPool/AndersonConjecture/Jensen/Construction/Transfinite.lean
View file
Open in desktop

Large diffs are not rendered by default.

740 changes: 338 additions & 402 deletions LeanPool/AndersonConjecture/Jensen/KrullDomain/HeightBound.lean
View file
Open in desktop

Large diffs are not rendered by default.

631 changes: 183 additions & 448 deletions LeanPool/AndersonConjecture/Jensen/KrullDomain/KrullDomain.lean
View file
Open in desktop

Large diffs are not rendered by default.

480 changes: 218 additions & 262 deletions LeanPool/AndersonConjecture/Jensen/KrullDomain/UFDConstruction.lean
View file
Open in desktop

Large diffs are not rendered by default.

Loading