OAI/GroupTheory/PolycyclicRecognition/GromovImport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Gromov’s polynomial-growth theorem in arbitrary universes.

  1. theorem OAI.PolycyclicRecognition.gromovPolynomialGrowthInput line 12

    Source documentation

    Polynomial word growth implies virtual nilpotence in every universe.

    theorem gromovPolynomialGrowthInput : GromovPolynomialGrowthInput J := by
…

    Mentions: OAI.PolycyclicRecognition.GromovPolynomialGrowthInput