Skip to content

feat: Add Kronecker-Weber Theorem problem#476

Open
bixbyr wants to merge 1 commit into
leanprover:mainfrom
bixbyr:add-kronecker-weber
Open

feat: Add Kronecker-Weber Theorem problem#476
bixbyr wants to merge 1 commit into
leanprover:mainfrom
bixbyr:add-kronecker-weber

Conversation

@bixbyr

@bixbyr bixbyr commented Jul 20, 2026

Copy link
Copy Markdown

feat: Add the Kronecker - Weber theorem. This states that every finite abelian extension of Q is contained in a cyclotomic field.

Co-authored-by: Gemini 3.1 Pro gemini@google.com

Co-authored-by: Gemini 3.1 Pro <gemini@google.com>
@bixbyr
bixbyr marked this pull request as ready for review July 21, 2026 03:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant