OAI/GroupTheory/PolycyclicRecognition/Algebra/AutomorphismExhaustion.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

An increasing union of inverse images under an automorphism

  1. def OAI.PolycyclicRecognition.automorphismStage line 15
  2. theorem OAI.PolycyclicRecognition.automorphismStage_zero line 18
  3. def OAI.PolycyclicRecognition.automorphismStageEquiv line 22
  4. theorem OAI.PolycyclicRecognition.automorphismStage_monotone line 25
  5. theorem OAI.PolycyclicRecognition.mem_automorphismStage_iff line 33
  6. theorem OAI.PolycyclicRecognition.automorphism_pow_mem_of_stable line 45
  7. theorem OAI.PolycyclicRecognition.automorphismStage_map_succ line 53
  8. theorem OAI.PolycyclicRecognition.automorphismStage_stable line 60
  9. theorem OAI.PolycyclicRecognition.automorphism_iSup_invariant line 68
  10. theorem OAI.PolycyclicRecognition.cohomologicalDimension_of_automorphism_exhaustion line 93
  11. theorem OAI.PolycyclicRecognition.torsionFree_of_automorphism_exhaustion line 102