Enumerating the elements of a subgroup of a finite group #
For a subgroup H of a finite group, Subgroup.fintypeOfFinite H is a Fintype structure on the
elements of H, so that finite sums and products can be indexed over H. Examples are the sum
over a subgroup in the relative norm, and the sums over a subgroup and its cosets in the transfer.
Main definitions #
Subgroup.fintypeOfFinite: theFintypestructureFintype.ofFiniteon the elements of a subgroup of a finite group.
@[instance_reducible]
noncomputable def
Subgroup.fintypeOfFinite
{G : Type u_1}
[Group G]
[Finite G]
(H : Subgroup G)
:
Fintype ↥H
The Fintype structure on a subgroup of a finite group given by Fintype.ofFinite.