---
tag: 3C53TD
kind: statement
role: theorem
name: Lagrange's theorem
msc: [20D60]
uses: [G5S1M9]
formal:
  - system: lean4
    library: mathlib
    decl: Subgroup.card_subgroup_dvd_card
    match: stronger
    adapter: Math2.Match.lagrange
sources:
  - book: isbn:9780471433347
    locator: Section 3.2, Theorem 8
---

## Statement

Let $G$ be a finite [[group|G5S1M9]] 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$.