Index of a Subgroup #
In this file we define the index of a subgroup, and prove several divisibility properties. Several theorems proved in this file are known as Lagrange's theorem.
Main definitions #
H.index
: the index ofH : Subgroup G
as a natural number, and returns 0 if the index is infinite.H.relindex K
: the relative index ofH : Subgroup G
inK : Subgroup G
as a natural number, and returns 0 if the relative index is infinite.
Main results #
card_mul_index
:Nat.card H * H.index = Nat.card G
index_mul_card
:H.index * Fintype.card H = Fintype.card G
index_dvd_card
:H.index ∣ Fintype.card G
relindex_mul_index
: IfH ≤ K
, thenH.relindex K * K.index = H.index
index_dvd_of_le
: IfH ≤ K
, thenK.index ∣ H.index
relindex_mul_relindex
:relindex
is multiplicative in towersMulAction.index_stabilizer
: the index of the stabilizer is the cardinality of the orbit
The index of an additive subgroup as a natural number. Returns 0 if the index is infinite.
If H
and K
are subgroups of an additive group G
, then relindex H K : ℕ
is the index of H ∩ K
in K
. The function returns 0
if the index is infinite.
Equations
- H.relindex K = (H.addSubgroupOf K).index
Alias of AddSubgroup.inf_eq_bot_of_coprime
.
Finite index implies finite quotient.
Equations
- Subgroup.fintypeOfIndexNeZero hH = Fintype.ofFinite (G ⧸ H)
Finite index implies finite quotient.
Equations
Alias of AddSubgroup.index_prod
.
Typeclass for finite index subgroups.
The subgroup has finite index
Typeclass for finite index subgroups.
The additive subgroup has finite index
A finite index subgroup has finite quotient.
Equations
A finite index subgroup has finite quotient