feat: add Brauer-Suzuki theorem eval problem#313
Open
kim-em wants to merge 3 commits into
Open
Conversation
This PR adds the 1959 Brauer-Suzuki theorem: if a finite group G has generalized quaternion Sylow 2-subgroups, then the unique involution of G maps to a central element of G/O(G). Historical precursor of Glauberman's Z*-theorem and a seed of the local-analysis programme. Introduces LeanEval/GroupTheory/Defs/OddCore.lean defining O(G) as the normal closure of the union of normal odd-order subgroups, since Mathlib has no `oddCore` operation. 🤖 Prepared with Claude Code
The original statement used `QuaternionGroup (2^(n-1))` with `n ≥ 2`,
which is mathematically correct but indexes Q_8, Q_16, ... by n = 2, 3,
... — not matching the textbook convention where n = log₂|P|.
Update to `QuaternionGroup (2^(n-2))` with `n ≥ 3`, so n cleanly equals
log₂|P| and the docstring's Q_{2^n} notation matches the index.
Spotted in second-opinion review by Codex.
🤖 Prepared with Claude Code
Switch to the more direct definition `sSup {N | N.Normal ∧ Odd (Nat.card N)}`,
matching the textbook formulation directly. The Normal instance is now
proved by `iSup_induction`: conjugation by `g` fixes every normal
subgroup in the indexing family, so it fixes their supremum.
🤖 Prepared with Claude Code
kim-em
force-pushed
the
eval/brauer-suzuki
branch
from
8f04f2b to
166be95
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds the 1959 Brauer-Suzuki theorem: if a finite group
Ghas generalized quaternion Sylow 2-subgroups, then the unique involution ofGmaps to a central element ofG/O(G). Historical precursor of Glauberman's Z*-theorem and a seed of the local-analysis programme.Introduces
LeanEval/GroupTheory/Defs/OddCore.leandefiningO(G)as the normal closure of the union of normal odd-order subgroups, since Mathlib has nooddCoreoperation.🤖 Prepared with Claude Code