OAI/GroupTheory/PolycyclicRecognition/Algebra/BoundedLocallyFiniteKernel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Removing a locally finite kernel with bounded finite subgroup orders

The bound on finite subgroups remains an explicit premise. Local finiteness then makes the whole kernel finite, and a finite kernel preserves virtual solvability by centralizing that kernel.

  1. def OAI.PolycyclicRecognition.HasBoundedFiniteSubgroupOrders line 17
  2. theorem OAI.PolycyclicRecognition.HasBoundedFiniteSubgroupOrders.subgroup line 20
  3. theorem OAI.PolycyclicRecognition.finite_of_locallyFinite_bounded line 30
  4. theorem OAI.PolycyclicRecognition.finite_locallyFinite_normal_subgroup line 49
  5. theorem OAI.PolycyclicRecognition.virtually_solvable_of_finite_kernel line 54
  6. theorem OAI.PolycyclicRecognition.virtually_solvable_of_finite_kernel_virtual_quotient line 80
  7. theorem OAI.PolycyclicRecognition.virtually_solvable_of_locallyFinite_kernel_bounded line 108