OAI/GroupTheory/PolycyclicRecognition/Algebra/CompatiblePrimitives.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compatible primitives along a countable tower

A primitive at the next stage can be corrected by a coboundary to agree with the previous one. This is the algebraic step in the dimension bound for a countable increasing union of subgroups.

  1. theorem OAI.PolycyclicRecognition.exists_compatible_primitives line 16