OAI/GroupTheory/PolycyclicRecognition/Algebra/SeparateFiniteIndexDensity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-index subgroups are dense in a connected polynomial group

A closed subgroup of finite index is open: its finite quotient is T1 and therefore discrete. The argument uses only continuous translations. In a connected group this forces the closure of every finite-index subgroup to be the whole group.

  1. theorem OAI.PolycyclicRecognition.separate_isOpen_of_closed_finiteIndex line 20
  2. theorem OAI.PolycyclicRecognition.separateClosure_eq_top_of_finiteIndex line 43