WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Finite group

Revision #1225 → #2426 · back to history

modifiedFinite group49450cf7cc19
FieldFrom #1225To #2426
mathlib.decl—Group
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Group.Defs
note—Mathlib has `Group` and expresses finiteness via a `Finite` (or `Fintype`) instance, together giving the notion of a finite group.
status—formalized
modifiedSymmetric group S_n43d9d81aa14b
FieldFrom #1225To #2426
mathlib.decl—Equiv.Perm
mathlib.match_kind—exact
mathlib.module—Mathlib.Logic.Equiv.Defs
note—`Equiv.Perm α` is the group of permutations of `α`; taking `α = Fin n` gives Sₙ.
status—formalized
modifiedOrder of symmetric groupff0a9b7c07df
FieldFrom #1225To #2426
mathlib.decl—Fintype.card_perm
mathlib.match_kind—exact
mathlib.module—Mathlib.Data.Fintype.Perm
note—`Fintype.card_perm` proves `Fintype.card (Perm α) = (Fintype.card α)!`.
status—formalized
modifiedCyclic group Z_n99451d6e8e8f
FieldFrom #1225To #2426
mathlib.decl—IsCyclic
mathlib.match_kind—exact
mathlib.module—Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
note—`IsCyclic` is the predicate that a group is generated by a single element; the concrete Z_n is `ZMod n`.
status—formalized
modifiedComplex nth roots of unity realization08ff0396fad4
FieldFrom #1225To #2426
mathlib.decl—rootsOfUnity.isCyclic
mathlib.match_kind—exact
mathlib.module—Mathlib.RingTheory.RootsOfUnity.Basic
note—`rootsOfUnity k R` defines the group of nth roots of unity in a commutative ring, and `rootsOfUnity.isCyclic` shows this group is cyclic in an integral domain.
status—formalized
addedCyclic group is isomorphic to nth roots of unity72e752d4ce6e
modifiedAbelian group29d16c506ca8
FieldFrom #1225To #2426
mathlib.decl—CommGroup
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Group.Defs
note—`CommGroup` (and `AddCommGroup`) are Mathlib's typeclasses for abelian groups.
status—formalized
modifiedStructure of finite abelian groupsddb8afedc83b
FieldFrom #1225To #2426
mathlib.decl—AddCommGroup.equiv_directSum_zmod_of_finite
mathlib.match_kind—exact
mathlib.module—Mathlib.GroupTheory.FiniteAbelian.Basic
note—This states any finite abelian group is a direct sum of `ZMod (p^n)` factors, i.e. the primary decomposition theorem.
status—formalized
modifiedGroup of Lie type2b1e973a077f
FieldFrom #1225To #2426
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no general notion of a group of Lie type / Chevalley group; only specific matrix groups like `SpecialLinearGroup` exist.
status—not_formalized
modifiedJordan's simplicity of PSL(2,q)664bdd774ca6
FieldFrom #1225To #2426
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No simplicity theorem for PSL(2, q) appears in Mathlib (loogle finds no `PSL.*simple` declarations).
status—not_formalized
modifiedLagrange's theoremc6f23cb78f62
FieldFrom #1225To #2426
mathlib.decl—Subgroup.card_subgroup_dvd_card
mathlib.match_kind—exact
mathlib.module—Mathlib.GroupTheory.Coset.Card
note—`Subgroup.card_subgroup_dvd_card` gives Lagrange's theorem: `Nat.card H ∣ Nat.card G`.
status—formalized
modifiedSylow theorems36bfebcaeee1
FieldFrom #1225To #2426
mathlib.decl—Sylow
mathlib.match_kind—exact
mathlib.module—Mathlib.GroupTheory.Sylow
note—Mathlib's `Sylow` file contains all three Sylow theorems: existence (`exists_subgroup_card_pow_prime`), conjugacy (`isPretransitive_of_finite`), and count (`card_sylow_modEq_one`).
status—formalized
modifiedCayley's theorem87e98fee6423
FieldFrom #1225To #2426
mathlib.decl—Equiv.Perm.subgroupOfMulAction
mathlib.match_kind—exact
mathlib.module—Mathlib.GroupTheory.Perm.Subgroup
note—Its docstring explicitly identifies it as "Cayley's theorem", giving the isomorphism `G ≃* range (toPermHom G G)`.
status—formalized
modifiedBurnside's theoremd9bfca0eeaa3
FieldFrom #1225To #2426
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Wikipedia refers to Burnside's `p^a q^b` solvability theorem; Mathlib only has Burnside's normal `p`-complement (transfer) theorem, which is a different result.
status—not_formalized
modifiedNon-abelian simple groups have order divisible by three primesa66a72d23b0b
FieldFrom #1225To #2426
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—This corollary of Burnside's `p^a q^b` theorem is not in Mathlib, since its parent theorem is not formalized.
status—not_formalized
modifiedFeit–Thompson theorema7483eb34f36
FieldFrom #1225To #2426
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Feit–Thompson odd-order theorem is not formalized in Mathlib (grep finds no matching declarations).
status—not_formalized
modifiedClassification of finite simple groups30c7609f9d44
FieldFrom #1225To #2426
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The CFSG is not in Mathlib; individual families (cyclic of prime order, alternating) are known simple but no unifying classification theorem exists.
status—not_formalized
modifiedJordan–Hölder theoremc41ac90a94cd
FieldFrom #1225To #2426
mathlib.decl—CompositionSeries.jordan_holder
mathlib.match_kind—generalization
mathlib.module—Mathlib.Order.JordanHolder
note—Mathlib proves Jordan–Hölder abstractly for any `JordanHolderLattice`, which specializes to the group-theoretic statement.
status—formalized
modifiedGroups of prime order are cyclic2e90b8718cf0
FieldFrom #1225To #2426
mathlib.decl—isCyclic_of_prime_card
mathlib.match_kind—exact
mathlib.module—Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
note—`isCyclic_of_prime_card` shows a finite group of prime cardinality is cyclic.
status—formalized
modifiedGroups of order p^243d3d15171f7
FieldFrom #1225To #2426
mathlib.decl—IsPGroup.isMulCommutative_of_card_eq_prime_sq
mathlib.match_kind——
mathlib.module—Mathlib.GroupTheory.PGroup
note—Mathlib proves a group of order p² is commutative, but the sharper `exactly two isomorphism types` classification is not present.
status—partial
modifiedGroups of order pq are cyclic360094256a1d
FieldFrom #1225To #2426
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No lemma stating groups of order `pq` (with `p ∤ q-1`) are cyclic is present; loogle/grep yield no matches.
status—not_formalized
modifiedSquarefree order implies solvable077a95ac0371
FieldFrom #1225To #2426
mathlib.decl—IsZGroup.of_squarefree
mathlib.match_kind—invocation
mathlib.module—Mathlib.GroupTheory.SpecificGroups.ZGroup
note—`IsZGroup.of_squarefree` combined with `IsZGroup.instIsSolvableOfFinite` yields solvability of any finite group of squarefree order.
status—formalized
modifiedAt most two simple groups of each order9f4d1ddf689a
FieldFrom #1225To #2426
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—This deep result depends on CFSG and is not in Mathlib.
status—not_formalized
addedInfinitely many orders with two non-isomorphic simple groups51cc8847bac1