OAI/GroupTheory/PolycyclicRecognition/Finiteness/HomologyRankOneLimit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integral rank-one properties of the exhausted top homology

  1. theorem OAI.PolycyclicRecognition.exists_pair_in_homology_stage line 14
  2. theorem OAI.PolycyclicRecognition.homology_commensurable_of_rankOne_stages line 32
  3. theorem OAI.PolycyclicRecognition.homology_torsionFree_of_rankOne_stages line 56
  4. theorem OAI.PolycyclicRecognition.rankOne_homology_map_eq_zero_of_nonzero_kernel line 74