Revision #1278 → #1832 · back to history
modifiedGroup (informal)47f79580c97e
| Field | From #1278 | To #1832 |
|---|
| note | The `Group` typeclass in Mathlib captures exactly the informal notion of a set with a binary operation satisfying the group axioms. | The `Group` typeclass in Mathlib captures the informal notion of a set with an associative binary operation, identity, and inverses. |
modifiedIntegers under addition5ae3bce6d4bb
| Field | From #1278 | To #1832 |
|---|
| anchors | [{"section":"First example: the integers","snippet":"One of the more familiar groups is the set of integers"},{"type":"math_alttext","value":"{\\displaystyle \\mathbb {Z} =\\{\\ldots ,-4,-3,-2,-1,0,1,2,3,4,\\ldots \\}}"}] | — |
| mathlib.decl | Int.instCommGroup | Int.instAddCommGroup |
| mathlib.module | Mathlib.Data.Int.Defs | Mathlib.Algebra.Group.Int.Defs |
| note | Mathlib equips `ℤ` with an `AddCommGroup` (and hence `AddGroup`) instance. | Mathlib equips `ℤ` with `Int.instAddCommGroup`, giving the standard additive group structure (the previously cited `Int.instCommGroup` does not exist). |
modifiedGroup (formal definition)238f9ad5f3b9
| Field | From #1278 | To #1832 |
|---|
| note | `class Group (G : Type u) extends DivInvMonoid G` is the direct formalization at `Mathlib/Algebra/Group/Defs.lean:1192`. | `class Group (G : Type u) extends DivInvMonoid G` in `Mathlib/Algebra/Group/Defs.lean` is the direct formalization. |
modifiedAbelian group9018b154f420
| Field | From #1278 | To #1832 |
|---|
| note | `class CommGroup extends Group, CommMonoid` at `Mathlib/Algebra/Group/Defs.lean:1275` (additive variant `AddCommGroup`). | `class CommGroup extends Group, CommMonoid` (additive variant `AddCommGroup`). |
modifiedUniqueness of inversesbb7f20d1f8cf
| Field | From #1278 | To #1832 |
|---|
| note | `left_inv_eq_right_inv` (and `inv_eq_of_mul_eq_one_right`) show any left/right inverse equals the canonical inverse. | `left_inv_eq_right_inv` shows any left inverse equals any right inverse, giving uniqueness of inverses. |
modifiedSubgroup04e81c4f24a4
| Field | From #1278 | To #1832 |
|---|
| note | `structure Subgroup (G : Type*) [Group G] extends Submonoid G` at `Mathlib/Algebra/Group/Subgroup/Defs.lean:295`. | `structure Subgroup (G : Type*) [Group G] extends Submonoid G` in `Mathlib/Algebra/Group/Subgroup/Defs.lean`. |
modifiedCosets and normal subgroupdde8c01bbe13
| Field | From #1278 | To #1832 |
|---|
| note | `Subgroup.Normal` is defined at line 605, and cosets are formalized via `QuotientGroup.leftRel` in `Mathlib.GroupTheory.Coset.Basic`. | `Subgroup.Normal` formalizes normal subgroups; cosets are formalized via `QuotientGroup.leftRel` in `Mathlib.GroupTheory.Coset.Defs`. |
modifiedLeft cosets form a partitionb4e40811e9bc
| Field | From #1278 | To #1832 |
|---|
| mathlib.module | Mathlib.GroupTheory.Coset.Basic | Mathlib.GroupTheory.Coset.Defs |
modifiedQuotient group3784300d51a5
| Field | From #1278 | To #1832 |
|---|
| anchors | [{"section":"Quotient groups","snippet":"is called a quotient group or factor group"},{"type":"math_alttext","value":"{\\displaystyle G/N=\\{gN\\mid g\\in G\\}}"}] | — |
| note | `G ⧸ N` with `[N.Normal]` carries a `Group` instance built via `QuotientGroup.con N`. | `G ⧸ N` with `[N.Normal]` carries a `Group` instance built via `QuotientGroup.Quotient.group`. |
modifiedNonzero rationals under multiplication6a1d968abc84
| Field | From #1278 | To #1832 |
|---|
| mathlib.module | Mathlib.Data.Rat.Defs | Mathlib.Algebra.Field.Rat |
| note | `ℚ` is a `Field`, so `ℚˣ` is a `CommGroup` under multiplication via the standard `Units` construction. | `ℚ` is a `Field` (via `Rat.instField`), so `ℚˣ` is a `CommGroup` under multiplication via the standard `Units` construction. |
modifiedModular addition group Z/nZ3c8746444a82
| Field | From #1278 | To #1832 |
|---|
| mathlib.module | Mathlib.Data.ZMod.Basic | Mathlib.Data.ZMod.Defs |
| note | `ZMod n` is the additive group ℤ/nℤ, with `quotientZMultiplesNatEquivZMod` showing `ℤ ⧸ ⟨n⟩ ≃+ ZMod n`. | `ZMod n` is the additive group ℤ/nℤ, with `Int.quotientZMultiplesNatEquivZMod` showing `ℤ ⧸ ⟨n⟩ ≃+ ZMod n`. |
modifiedMultiplicative group of integers modulo a primec447fb1806d9
| Field | From #1278 | To #1832 |
|---|
| anchors | [{"section":"Modular arithmetic","snippet":"there is also the multiplicative group of integers modulo"},{"type":"math_alttext","value":"{\\displaystyle a\\cdot b\\equiv 1{\\pmod {p}},}"}] | — |
| mathlib.module | Mathlib.Data.ZMod.Units | Mathlib.Data.ZMod.Basic |
| note | `(ZMod p)ˣ` is the unit group; cardinality and structure are developed in `Mathlib.Data.ZMod.Units`. | `(ZMod p)ˣ` is the unit group; `ZMod.unitsEquivCoprime` characterises units as coprime residues. |
modifiedCyclic group1d967083eed1
| Field | From #1278 | To #1832 |
|---|
| anchors | [{"section":"Cyclic groups","snippet":"A cyclic group is a group all of whose elements are powers of a particular element"},{"type":"math_alttext","value":"{\\displaystyle \\dots ,a^{-3},a^{-2},a^{-1},a^{0},a,a^{2},a^{3},\\dots ,}"},{"type":"math_alttext","value":"{\\displaystyle \\dots ,(-a)+(-a),-a,0,a,a+a,\\dots .}"}] | — |
| note | `class IsCyclic (G : Type u) [Pow G ℤ] : Prop` at `Mathlib/Algebra/Group/Defs.lean:1028` asserts every element is a power of a generator. | `class IsCyclic` in `Mathlib.Algebra.Group.Defs` asserts every element is a power of a generator. |
modifiedGroup of nth roots of unity103264566d1e
| Field | From #1278 | To #1832 |
|---|
| note | `rootsOfUnity n M` is the subgroup of `Mˣ` of n-th roots of unity; `rootsOfUnity.isCyclic` proves cyclicity over an integral domain. | `rootsOfUnity n M` is the subgroup of `Mˣ` of n-th roots of unity, with cyclicity proved over integral domains. |
modifiedInfinite cyclic group is isomorphic to Z0befe35c6471
| Field | From #1278 | To #1832 |
|---|
| note | `intCyclicMulEquiv : Multiplicative ℤ ≃* G` (and additive variant `intCyclicAddEquiv`) realize the isomorphism for any infinite cyclic group. | `intCyclicMulEquiv : Multiplicative ℤ ≃* G` realises the isomorphism for any infinite cyclic group. |
modifiedGroup actionfe168c28c5be
| Field | From #1278 | To #1832 |
|---|
| note | `class MulAction (α β) [Monoid α]` formalizes group/monoid actions; specialized to a group it is the standard notion. | `class MulAction (α β) [Monoid α]` formalizes group/monoid actions; specialised to a group it is the standard notion. |
modifiedGalois group of the quadratic73d712656d9e
| Field | From #1278 | To #1832 |
|---|
| anchors | [{"section":"Galois groups","snippet":"the solutions of the quadratic equation"},{"type":"math_alttext","value":"{\\displaystyle x={\\frac {-b\\pm {\\sqrt {b^{2}-4ac}}}{2a}}.}"}] | — |
modifiedCayley's theorem5167e2a5f751
| Field | From #1278 | To #1832 |
|---|
| note | `MulAction.toPermHom G G : G →* Equiv.Perm G` gives the Cayley embedding, but I did not find a named lemma asserting injectivity as 'Cayley's theorem'. | `MulAction.toPermHom G G : G →* Equiv.Perm G` provides the Cayley embedding, but no named lemma asserting injectivity as 'Cayley's theorem' was located. |
modifiedOrder of an elementd7075726d1d3
| Field | From #1278 | To #1832 |
|---|
| anchors | [{"section":"Finite groups","snippet":"The order of an element"},{"type":"math_alttext","value":"{\\displaystyle \\underbrace {a\\cdots a} _{n{\\text{ factors}}},}"}] | — |
| note | `orderOf x` is defined at `Mathlib/GroupTheory/OrderOfElement.lean:180` as the smallest positive n with `x^n = 1`. | `orderOf x` is the smallest positive n with `x^n = 1` (or 0 if none), defined in `Mathlib.GroupTheory.OrderOfElement`. |
modifiedLagrange's theoreme71719ffaea1
| Field | From #1278 | To #1832 |
|---|
| mathlib.module | Mathlib.GroupTheory.Index | Mathlib.GroupTheory.Coset.Card |
| note | `card_subgroup_dvd_card` states |H| divides |G| for a subgroup H of a finite group G. | `Subgroup.card_subgroup_dvd_card` states |H| divides |G| for a subgroup H of a finite group G. |
modifiedGroups of prime order are cyclic3d7ae2fc1e20
| Field | From #1278 | To #1832 |
|---|
| mathlib.module | Mathlib.GroupTheory.SpecificGroups.Cyclic | Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic |
modifiedSimple groupa3a7f3e45d23
| Field | From #1278 | To #1832 |
|---|
| note | `class IsSimpleGroup : Prop extends Nontrivial G` at `Mathlib/GroupTheory/Subgroup/Simple.lean:38`. | `class IsSimpleGroup : Prop extends Nontrivial G` characterises simple groups via their normal-subgroup lattice. |
modifiedGeneral linear group as a Lie group22ac1fcdd5cc
| Field | From #1278 | To #1832 |
|---|
| anchors | [{"section":"Lie groups","snippet":"A standard example is the general linear group introduced above"},{"type":"math_alttext","value":"{\\displaystyle \\det(A)\\neq 0,}"}] | — |
| mathlib.module | Mathlib.LinearAlgebra.GeneralLinearGroup.Basic | Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs |
| note | GLₙ is defined and the smooth-manifold/Lie-group instance machinery exists, but I did not locate an explicit `LieGroup` instance on `GL n ℝ`. | GLₙ is defined and the smooth-manifold/Lie-group machinery exists, but I did not locate an explicit `LieGroup` instance on `GL n ℝ`. |
modifiedMonoid (relaxation)7ff9b735fd7a
| Field | From #1278 | To #1832 |
|---|
| note | `class Monoid extends Semigroup, MulOneClass` at `Mathlib/Algebra/Group/Defs.lean:652`. | `class Monoid extends Semigroup, MulOneClass` formalises monoids in `Mathlib.Algebra.Group.Defs`. |
addedAssociativity47651355fff9
addedCategory of groupsc5ea2a94fe74
addedIdentity homomorphism7da11da89530
addedFree group83da400d4c59
addedCayley graph1665e8618581
addedFundamental group6522134455c3
addedCenter of a group133d997f4dfc
addedCommutator subgroup636c1ab85265
addedSylow theoremsaf5d0a970995
addedJordan–Hölder theorema37ba1c22425
addedGrothendieck groupaf2c074401cd
addedSpecial orthogonal group SO(n)7246133edd2c
addedGroup object in a categoryab49c02c0ac0