OAI/GroupTheory/PolycyclicRecognition/Algebra/SeparateIrreducibleComponent.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The irreducible identity component of a separately continuous group

Separate continuity suffices for products of irreducible sets. Consequently the irreducible component of the identity is a normal subgroup, and it has finite index in a Noetherian group.

  1. theorem OAI.PolycyclicRecognition.preirreducible_image2_of_separate_continuity line 19
  2. theorem OAI.PolycyclicRecognition.preirreducible_subset_identityComponent line 37
  3. def OAI.PolycyclicRecognition.separateIrreducibleComponent line 53
  4. instance OAI.PolycyclicRecognition.separateIrreducibleComponent_normal line 73
  5. theorem OAI.PolycyclicRecognition.separateIrreducibleComponent_closed line 81
  6. instance OAI.PolycyclicRecognition.separateIrreducibleComponent_irreducible line 84
  7. theorem OAI.PolycyclicRecognition.inverse_mul_mem_identityComponent_of_component_eq line 88
  8. theorem OAI.PolycyclicRecognition.separateIrreducibleComponent_finiteIndex line 99
  9. theorem OAI.PolycyclicRecognition.noetherian_preconnected_group_irreducible line 117