Group theory · existing Mathlib theorem

Lagrange's Theorem

For a subgroup inside a group, Mathlib's natural-number cardinality of the subgroup divides the natural-number cardinality of the whole group.

groups
subgroups
cardinality
divisibility

Four separate status axes

Upstream indexedPinned source bytes verified locally

Locally reproducedExact upstream declaration replayed

Reviewed pageCurrent public presentation reviewed

Accepted Atlas resultNot recorded for the preferred artifact

These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.

Formal orientation

Statement map

This deterministic map orients the reader from the mathematical summary to the pinned declaration and exact checked form. The HTML statement below is authoritative.

The theorem at a glance

Lagrange's Theorem at a glance

A source-bound editorial overview of the exact Mathlib formulation. The image is explanatory; the statement map, formal type, and pinned source remain authoritative.

An ivory theorem poster shows a subgroup inside an ambient group, repeated equal cosets, and the exact Nat.card divisibility statement, with separate finite-case intuition and infinite-type convention panels. — Equal cosets motivate the familiar finite case while the poster keeps Mathlib's finiteness-free Nat.card divisibility form authoritative.

One emerald subgroup cluster is surrounded by seven congruent cobalt clusters that tile a larger circular group. — Equal-size translated clusters suggest how subgroup cardinality divides the ambient group cardinality.

Complementary intuition

A mathematical landmark

Lagrange's theorem is one of the first structural results in group theory. In the familiar finite case it tightly constrains possible subgroup sizes and element orders.

The low-text schematic gives the theorem a visual identity; it does not replace the source-bound poster or exact statement.

Authoritative formal type

Exact Mathlib statement

Subgroup.card_subgroup_dvd_card {α : Type u} [Group α] (s : Subgroup α) : Nat.card s ∣ Nat.card α

Selected evidence declaration text

theorem Subgroup.card_subgroup_dvd_card {α : Type u} [Group α] (s : Subgroup α) : Nat.card s ∣ Nat.card α

Proof architecture

From quotient–subgroup pairs to divisibility

2 curated stages

Mathlib obtains the exact Nat.card product identity from the equivalence between the ambient group and quotient–subgroup pairs, then simplifies that identity to the divisibility statement. The familiar equal-coset picture is finite-case intuition; the declaration itself has no explicit finiteness hypothesis.

These source-anchored stages explain the retained Mathlib proof route. They are generated explanations, not proof evidence or an extracted Lean proof-term dependency graph.

Pair quotient positions with subgroup elements
Pair quotient positions with subgroup elements
The quotient–subgroup product equivalence pairs each coset position with one subgroup element, yielding the ambient natural-cardinality product.
Open original image in a new tab
The quotient–subgroup product equivalence pairs each coset position with one subgroup element, yielding the ambient natural-cardinality product.
Nat.card α = Nat.card (α ⧸ s) * Nat.card s
The equivalence Subgroup.groupEquivQuotientProdSubgroup identifies the ambient group with the product of its left-coset quotient and the subgroup. Nat.card_congr together with Nat.card_prod converts that equivalence into the exact natural-cardinality product identity.
Read the product identity as divisibility
Read the product identity as divisibility
Because the ambient natural cardinality is a whole multiple of the subgroup natural cardinality, the subgroup cardinality divides it.
Open original image in a new tab
Because the ambient natural cardinality is a whole multiple of the subgroup natural cardinality, the subgroup cardinality divides it.
Nat.card s ∣ Nat.card α
The final simp step rewrites the product identity and applies dvd_mul_left, using Nat.card of the quotient as the multiplier. This proves Nat.card s divides Nat.card α without adding a finiteness hypothesis or asserting a separate index formula.

Claim boundary

No new theorem is claimed

This is Mathlib's Nat.card divisibility formulation. The declaration has no explicit finiteness hypothesis, and the page does not replace its exact type with a stronger index formula or claim a new proof.

Proof Atlas did not originate Lagrange's theorem or Mathlib's declaration.
The local run reproduces the exact upstream declaration; it is not a local wrapper.
A successful local check does not by itself create an accepted Atlas result.

Provenance

Origin and evidence stay separate

Existing declaration: Subgroup.card_subgroup_dvd_card in mathlib
Relationship: The checked artifact is the upstream declaration itself
Preferred checked artifact: artifact.library.mathlib.lagrange-theorem.v001
Source handling: Verified upstream reference; no mirrored source package