OAI/GroupTheory/PolycyclicRecognition/Algebra/CyclicKernelGrowth.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Growth drops in the kernel of a surjection to the integers

Distinct integer heights give disjoint translates of a kernel word ball. The count supplies the degree drop required by the Gromov induction.

  1. theorem OAI.PolycyclicRecognition.cyclic_kernel_wordBall_count line 15
  2. theorem OAI.PolycyclicRecognition.cyclic_kernel_word_growth_degree_drop line 49