OAI/GroupTheory/PolycyclicRecognition/Algebra/CharacterTamenessEndgame.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite character tameness supplies a contracting group element

The finite zero-sum obstruction is converted to an actual integral separating element, and then to the already proved nilpotent finiteness endgame.

  1. theorem OAI.PolycyclicRecognition.exists_character_hemisphere_of_no_zero_sum line 19
  2. theorem OAI.PolycyclicRecognition.virtualSolvableFiniteDimension_of_character_tameness line 44