Theorems · Definition · group theory

Subgroup.index

{G : Type u_1} → [inst : Group G] → Subgroup G → ℕ

The index of a subgroup as a natural number. Returns 0 if the index is infinite. [Wikidata Q1464168](https://www.wikidata.org/wiki/Q1464168)

Defined in

Mathlib.GroupTheory.Index

Cited by

150 results in Mathlib

Foundations

Depth 90 from the axioms, rests on 2,531 definitions · uses propext, Classical.choice, Quot.sound

Assumes

Group