OAI/GroupTheory/PolycyclicRecognition/Algebra/CharacteristicKernelQuotient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The kernel after quotienting by a characteristic subgroup

The comparison does not require the characteristic subgroup to have finite index. In particular it applies to the full nilpotent torsion subgroup.

  1. def OAI.PolycyclicRecognition.characteristicKernelQuotientEquiv line 15