OAI/GroupTheory/PolycyclicRecognition/Algebra/AscendingCoinvariantRelations.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Coinvariant relations are detected in a finite subgroup stage

For an ascending exhaustion of a group, a linear combination of coinvariant relations uses only finitely many group elements. It therefore already lies in the relations of one stage of the exhaustion.

  1. abbrev OAI.PolycyclicRecognition.subgroupCoinvariantRelations line 18
  2. theorem OAI.PolycyclicRecognition.subgroupCoinvariantRelations_mono line 21
  3. theorem OAI.PolycyclicRecognition.subgroupCoinvariantRelations_le line 27
  4. theorem OAI.PolycyclicRecognition.subgroupCoinvariantRelations_exhaustion line 33
  5. theorem OAI.PolycyclicRecognition.coinvariantRelations_exhaustion line 53