Lagrange's theorem

Lagrange's theorem
Tag	`3C53TD`
URI	`m2://3C53TD`
Kind	statement, theorem
Writing	W0 stub
MSC	20D60
Status	This copy of the site has no build data. Run `m2 status 3C53TD`.
Uses	Group
Formal	`Subgroup.card_subgroup_dvd_card` lean4, stronger match

Markdown · JSON · Edit

Statement

Let $G$ be a finite group and let $H$ be a subgroup of $G$ . Then the order of $H$ divides the order of $G$ .

Remarks

The quotient $|G| / |H|$ is the number of left cosets of $H$ in $G$ .

What this node needs for W1

an inventory row: the row of the inventory that the node accounts for (0 of 1)

The writing levels say how complete the text of a node is. They do not measure its truth.

What this needs

To read this node, read these 2 nodes in this order. The foundations come first, and the list ends with this node.

Each node uses the nodes above it. The colour of the bar on a box shows the evidence level, and the box also gives it as text. The list below has the same nodes.

no evidence level

Group concept
Lagrange's theorem statement

What depends on this

19 nodes use this node, directly or through other nodes.

A finite group is nilpotent iff it is the product of its Sylow subgroups 00Y9N80VSS
Groups of prime order are cyclic 05MM4EK4SA
Order of an element divides the order of the group 08V7JHS3QZ
Fixed points of a p-group action 098D2E7DEH
Second Sylow theorem 09GCQ5STVJ
Groups of order p squared are abelian 09JZ9P4899
The number of Sylow subgroups is the index of the normaliser 09ZJ6CAK7S
The alternating group A5 is simple 0GKQKF0FXJ
Abelian simple groups have prime order 0JJV80RXHD
Cauchy's theorem 0JM7PA288B
The number of Sylow subgroups divides the index 0M3PYJ3TSE
Converse of Lagrange's theorem fails for the alternating group A4 0PDBVPP233
Third Sylow theorem 0Q8DGAZSJ4
Frattini argument 0QTZDKJEDV
Size of an orbit times the size of the stabiliser 0S19CWFZM2
First Sylow theorem 0V98WY94B8
Groups of order pq 0YBR6QPY4Y
Burnside's lemma 0Z47M1B2VS
g to the order of the group is the identity 0ZEPNS9BXK

Sources

Book isbn:9780471433347, Section 3.2, Theorem 8

What links here

Used by

Groups of prime order are cyclic 05MM4EK4SA
Order of an element divides the order of the group 08V7JHS3QZ
Groups of order p squared are abelian 09JZ9P4899
The alternating group A5 is simple 0GKQKF0FXJ
Cauchy's theorem 0JM7PA288B
Converse of Lagrange's theorem fails for the alternating group A4 0PDBVPP233
Size of an orbit times the size of the stabiliser 0S19CWFZM2