Module

PGroupFormation.lean

Nyll.ProCGroups.FiniteGroups.PGroupFormation

1 declaration indexed from sourceView source ↗

Module documentation

The full formation of finite p-groups

The existing formation, subgroup closure and extension closure proofs supply the full-formation property used by maximal pro-p residual quotients.

Imports1

Nyll.ProCGroups.FiniteGroups.StandardClasses

Imported by9

theorem

pGroup_fullFormation

L20 ↗

ProCGroups.FiniteGroupClass.pGroup_fullFormation

Documentation

Finite p-groups form a full formation, using their established subgroup and extension closure properties.

Source context 1 command

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

namespace ProCGroups.FiniteGroupClass

Lean source · full declaration

theorem pGroup_fullFormation (p : ℕ) [Fact p.Prime] : FullFormation (pGroup p) where
  melnikovFormation :=
    { formation := pGroup_formation p
      normalSubgroupClosed := fun N _ hG => pGroup_subgroupClosed p N hG
      extensionClosed := pGroup_extensionClosed p }
  subgroupClosed := pGroup_subgroupClosed p

Module documentation

The full formation of finite p-groups

Declarations

pGroup_fullFormation