OAI/GroupTheory/PolycyclicRecognition/Finiteness/CyclicTopHomologyInjection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The top homology injection for an infinite cyclic quotient

  1. def OAI.PolycyclicRecognition.cyclicTopHomologyInjection line 13
  2. instance OAI.PolycyclicRecognition.cyclicTopHomologyInjection_mono line 24
  3. theorem OAI.PolycyclicRecognition.integralRankOne_properties_of_injective line 40