Prove2Me

Coset_Cardinality

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

The cardinality of a subgroup H divides the cardinality of a finite group G, because left cosets of H partition G and each coset has the same cardinality as H.

Preamble
import Mathlib.GroupTheory.Coset.Basic
import Mathlib.GroupTheory.Index
import Mathlib.Tactic
Formal statement
theorem Coset_Cardinality {G : Type _} [Group G] [Fintype G] (H : Subgroup G) [Fintype H] : Fintype.card H ∣ Fintype.card G := by sorry

View graph