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 * Nat.card H = Nat.card G
index_dvd_card
:H.index ∣ Nat.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.
Instances For
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
Instances For
Alias of Subgroup.relIndex
.
If H
and K
are subgroups of a group G
, then relIndex H K : ℕ
is the index
of H ∩ K
in K
. The function returns 0
if the index is infinite.
Equations
Instances For
Alias of Subgroup.relIndex_map_map_of_injective
.
Alias of Subgroup.relIndex_dvd_index_of_le
.
Alias of Subgroup.relIndex_subgroupOf
.
Alias of Subgroup.inf_relIndex_right
.
Alias of Subgroup.inf_relIndex_left
.
Alias of Subgroup.relIndex_sup_right
.
Alias of Subgroup.relIndex_sup_left
.
Alias of Subgroup.relIndex_dvd_index_of_normal
.
Alias of Subgroup.relIndex_top_left
.
Alias of Subgroup.relIndex_top_right
.
Alias of Subgroup.relIndex_bot_left
.
Alias of Subgroup.relIndex_bot_right
.
Alias of Subgroup.relIndex_self
.
Alias of Subgroup.relIndex_dvd_card
.
If J
has finite index in K
, then the same holds for their comaps under any
additive group hom.
Alias of Subgroup.relIndex_comap_ne_zero
.
If J
has finite index in K
, then the same holds for their comaps under any group hom.
If J
has finite index in K
, then J ⊓ L
has finite index in K ⊓ L
for any
L
.
Alias of Subgroup.relIndex_inter_ne_zero
.
If J
has finite index in K
, then J ⊓ L
has finite index in K ⊓ L
for any L
.
Alias of Subgroup.relIndex_iInf_ne_zero
.
Alias of Subgroup.relIndex_eq_one
.
Finite index implies finite quotient.
Equations
- Subgroup.fintypeOfIndexNeZero hH = Fintype.ofFinite (G ⧸ H)
Instances For
Finite index implies finite quotient.
Equations
Instances For
Alias of AddSubgroup.index_prod
.
Alias of Subgroup.relIndex_toAddSubgroup
.
Alias of AddSubgroup.relIndex_toSubgroup
.
Typeclass for finite index subgroups.
The additive subgroup has finite index; recall that
AddSubgroup.index
returns 0 when the index is infinite.
Instances
Typeclass for finite index subgroups.
The subgroup has finite index; recall that
Subgroup.index
returns 0 when the index is infinite.
Instances
Alias of Subgroup.FiniteIndex.index_ne_zero
.
The subgroup has finite index;
recall that Subgroup.index
returns 0 when the index is infinite.
Typeclass for a subgroup H
to have finite index in a subgroup K
.
Instances
Alias of Subgroup.relIndex_ne_zero
.
A finite index subgroup has finite quotient.
Instances For
A finite index subgroup has finite quotient
Instances For
Alias of Subgroup.relIndex_pointwise_smul
.
Alias of AddSubgroup.relIndex_pointwise_smul
.