OAI/GroupTheory/PolycyclicRecognition/Algebra/SmallCoefficientFiniteIndex.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The small coefficient ring over finite-index subgroups

Relative coset indicators provide an actual trace-one element. Restriction to an integer-finite-dimensional subgroup therefore bounds the dimension of the ring over the larger subgroup, without requiring normality.

  1. def OAI.PolycyclicRecognition.smallCoefficientRelativeTransversal line 22
  2. theorem OAI.PolycyclicRecognition.smallCoefficientRelativeTransversal_apply line 27
  3. theorem OAI.PolycyclicRecognition.smallCoefficientRelativeTransversal_invariant line 32
  4. theorem OAI.PolycyclicRecognition.rightCoset_representative_mul_mem_iff line 42
  5. theorem OAI.PolycyclicRecognition.smallCoefficientRelativeTransversal_trace_one line 57
  6. theorem OAI.PolycyclicRecognition.smallCoefficient_finiteIndex_dimension_le line 84