OAI/GroupTheory/PolycyclicRecognition/Algebra/SeparateGroupClosure.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Closures and components using separately continuous multiplication

Polynomial matrix groups have this weaker topological structure. It is enough to form subgroup closures and the normal identity component. In a Noetherian space the latter has finite index.

  1. def OAI.PolycyclicRecognition.separateClosure line 20
  2. theorem OAI.PolycyclicRecognition.separateClosure_closed line 28
  3. theorem OAI.PolycyclicRecognition.separateClosure_mono line 31
  4. theorem OAI.PolycyclicRecognition.separateClosure_normal line 34
  5. def OAI.PolycyclicRecognition.separateIdentityComponent line 41
  6. instance OAI.PolycyclicRecognition.separateIdentityComponent_normal line 55
  7. theorem OAI.PolycyclicRecognition.separateIdentityComponent_closed line 63
  8. theorem OAI.PolycyclicRecognition.separateIdentityComponent_preconnected line 66
  9. theorem OAI.PolycyclicRecognition.separateIdentityComponent_finiteIndex line 69