OAI/GroupTheory/PolycyclicRecognition/CoarseFiniteGeneration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite generation is preserved by discrete-group coarse equivalence.

  1. theorem OAI.PolycyclicRecognition.GroupCoarseEquivalence.finitelyGenerated line 14

    Source documentation

    Coarse connectedness, expressed by finite generation, transfers through the finite-difference control and finite error sets of a coarse equivalence.

    theorem GroupCoarseEquivalence.finitelyGenerated (e : GroupCoarseEquivalence G H)
    [Group.FG G] : Group.FG H := by
…

    Mentions: OAI.PolycyclicRecognition.GroupCoarseEquivalence