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
index_eq_mul_of_le
: IfH ≤ K
, thenH.index = K.index * (H.subgroupOf K).index
index_dvd_of_le
: IfH ≤ K
, thenK.index ∣ H.index
relindex_mul_relindex
:relindex
is multiplicative in towers
The index of a subgroup as a natural number, and returns 0 if the index is infinite.
Instances For
The relative index of a subgroup as a natural number, and returns 0 if the relative index is infinite.
Instances For
An additive subgroup has index two if and only if there exists a
such that
for all b
, exactly one of b + a
and b
belong to H
.
Instances For
Finite index implies finite quotient.
Instances For
Finite index implies finite quotient.
Instances For
- finiteIndex : Subgroup.index H ≠ 0
The subgroup has finite index
Typeclass for finite index subgroups.
Instances
- finiteIndex : AddSubgroup.index H ≠ 0
The additive subgroup has finite index
Typeclass for finite index subgroups.
Instances
A finite index subgroup has finite quotient
Instances For
A finite index subgroup has finite quotient.