NYLL
Module

InducedFunctions.lean

Nyll.ProCGroups.FiniteGroups.InducedFunctions
2 declarations indexed from sourceView source ↗

Module documentation

Finite-class preservation for induced groups

The induced group is a subgroup of the finite product of copies of its coefficient group. This gives Sigma membership and preserves finite abelian exponent bounds without a choice of coset representatives.

Imports2
Imported by1

Declarations

theorem

induced_sigmaGroup

L27 ↗
ProCGroups.InducedFunctions.induced_sigmaGroup
Documentation

Induction along a subgroup of a finite group preserves finite Sigma groups. Its commutative group structure is inherited from the function group.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.InducedFunctions
universe u
variable {G B : Type u} [Group G] [Finite G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
Lean source · statement
theorem induced_sigmaGroup (sigma : Set ℕ)
    (hB : FiniteGroupClass.sigmaGroup sigma B) :
    FiniteGroupClass.sigmaGroup sigma (InducedModule (B := B) H)
theorem

induced_abelianExponent

L37 ↗
ProCGroups.InducedFunctions.induced_abelianExponent
Documentation

Induction along a subgroup of a finite group preserves finite abelian groups of exponent dividing n, including elementary abelian prime groups.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.InducedFunctions
universe u
variable {G B : Type u} [Group G] [Finite G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
Lean source · statement
theorem induced_abelianExponent (n : ℕ)
    (hB : FiniteGroupClass.abelianExponent n B) :
    FiniteGroupClass.abelianExponent n (InducedModule (B := B) H)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.