Revision #2412 → #3103 · back to history
modifiedQuartic with Galois group the Klein four-group97fd7ac34da3
| Field | From #2412 | To #3103 |
|---|
| note | Mathlib has `KleinFour` and `Polynomial.Gal`, but no worked quartic example identifying its Galois group with the Klein four-group. | Mathlib has `IsKleinFour` and `Polynomial.Gal`, but no worked quartic example identifying its Galois group with the Klein four-group. |
modifiedExistence of non-solvable polynomials for n > 4f5b85052f454
| Field | From #2412 | To #3103 |
|---|
| note | No theorem in Mathlib asserts existence of degree-`n` polynomials (for each `n > 4`) that are not solvable by radicals. | Mathlib's `AbelRuffini` file only formalizes the easy direction (`solvableByRad ⇒ IsSolvable Gal`); no concrete non-solvable quintic (nor a uniform 'for every n>4' existence theorem) is present. |
| provenance | ai | ai-moderated |
modifiedSymmetric group S_n is not solvable for n ≥ 533a86b5955e8
| Field | From #2412 | To #3103 |
|---|
| mathlib.decl | Equiv.Perm.not_solvable | Equiv.Perm.not_isSolvable |
| note | Mathlib proves `Equiv.Perm.not_solvable` for cardinality ≥ 5, via simplicity of the alternating group `alternatingGroup.isSimple` for n ≥ 5. | Mathlib proves `Equiv.Perm.not_isSolvable` for cardinality ≥ 5 (with alias `Equiv.Perm.not_solvable`), via simplicity of the alternating group `alternatingGroup.isSimpleGroup` for n ≥ 5. |
modifiedNon-solvable quintic x^5 − x − 1504009de606d
| Field | From #2412 | To #3103 |
|---|
| note | Mathlib has no proof that `X^5 - X - 1` (or any specific quintic) has non-solvable Galois group. | Mathlib has no concrete Abel–Ruffini witness polynomial (neither Van der Waerden's `X^5 - X - 1` nor any other) proved to have non-solvable Galois group. |
| provenance | ai | ai-moderated |
modifiedCayley's theorembfbb3e658957
| Field | From #2412 | To #3103 |
|---|
| note | Cayley's theorem is realized via the left-regular action embedding `G ↪ Equiv.Perm G`; see also `Subgroup.equivMapOfInjective` and the standard embedding into `Equiv.Perm`. | Cayley's theorem is realized via the left-regular action embedding `G ↪ Equiv.Perm G` obtained from `MulAction.toPermHom` applied to the regular action. |
modifiedAlternating group A_n is simple for n ≥ 5c1610f10dc1e
| Field | From #2412 | To #3103 |
|---|
| mathlib.decl | alternatingGroup.isSimpleGroup_five | alternatingGroup.isSimpleGroup |
| note | Simplicity of `alternatingGroup (Fin n)` for `n ≥ 5` is formalized; this is the key group-theoretic input behind `Equiv.Perm.not_solvable` and Abel–Ruffini. | `alternatingGroup.isSimpleGroup` proves `IsSimpleGroup (alternatingGroup α)` whenever `5 ≤ Nat.card α`; this is the key group-theoretic input behind `Equiv.Perm.not_isSolvable` and Abel–Ruffini. |
addedAlgebraic closure of a field5dc1756b7938
addedSeparable field extension7c44e8401bd1
addedRational root theorem80fd593ddfcd
addedFixed field of a subgroupa719fb143774
addedPrimitive n-th root of unity4d98abf9b8d7