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 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.
Equations
- H.relindex K = (H.addSubgroupOf K).index
Instances For
Alias of Subgroup.index_bot
.
Alias of Subgroup.relindex_bot_left
.
Alias of Subgroup.card_dvd_of_injective
.
Alias of Subgroup.card_dvd_of_surjective
.
Finite index implies finite quotient.
Equations
Instances For
Finite index implies finite quotient.
Equations
- Subgroup.fintypeOfIndexNeZero hH = Fintype.ofFinite (G ⧸ H)
Instances For
Typeclass for finite index subgroups.
- finiteIndex : H.index ≠ 0
The additive subgroup has finite index
Instances
The additive subgroup has finite index
A finite index subgroup has finite quotient
Equations
- H.fintypeQuotientOfFiniteIndex = AddSubgroup.fintypeOfIndexNeZero ⋯
Instances For
A finite index subgroup has finite quotient.
Equations
- H.fintypeQuotientOfFiniteIndex = Subgroup.fintypeOfIndexNeZero ⋯
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯