Module

PrimeSigma.lean

Nyll.ProCGroups.FiniteGroups.PrimeSigma

2 declarations indexed from sourceView source ↗

Module documentation

The finite class equality identifies the actual residual cores and maximal quotients used by the singleton-Sigma and pro-p formulations.

Imports3

Imported by2

theorem

ProCGroups.FiniteGroupClass.sigmaGroup_singleton_iff_pGroup

Documentation

A finite group has no prime divisors outside {p} exactly when it is a finite p-group.

Source context 2 commands

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

namespace ProCGroups.FiniteGroupClass
universe u

Lean source · statement

theorem sigmaGroup_singleton_iff_pGroup (p : ℕ) [Fact p.Prime]
    (G : Type u) [Group G] : sigmaGroup {p} G ↔ pGroup p G

theorem

ProCGroups.FiniteGroupClass.sigmaGroup_singleton_eq_pGroup

Documentation

Equality of the bundled finite classes also identifies their actual maximal residual quotient constructions, without a comparison hypothesis.

Source context 2 commands

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

namespace ProCGroups.FiniteGroupClass
universe u

Lean source · statement

theorem sigmaGroup_singleton_eq_pGroup (p : ℕ) [Fact p.Prime] :
    sigmaGroup.{u} {p} = pGroup.{u} p