OAI/GroupTheory/PolycyclicRecognition/Finiteness/CompletedIdentityTorsion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Torsion of the complete identity bounds all finite subgroup orders

The annihilator is kept as an explicit premise. In particular, the theorem below does not claim that FP-infinity by itself supplies an annihilator.

  1. theorem OAI.PolycyclicRecognition.normalizedStableScalar_restrict_descend line 21
  2. theorem OAI.PolycyclicRecognition.finite_subgroup_order_dvd_of_completedIdentity_annihilator line 45
  3. theorem OAI.PolycyclicRecognition.boundedFiniteSubgroupOrders_of_completedIdentity_torsion line 78