OAI/GroupTheory/PolycyclicRecognition/Algebra/CayleyWordMaps.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Word balls under homomorphisms

Image word balls are literal finite images, so polynomial growth descends to the matrix image constructed by the harmonic argument.

  1. theorem OAI.PolycyclicRecognition.wordBall_image line 13
  2. theorem OAI.PolycyclicRecognition.wordBall_image_card_le line 43
  3. theorem OAI.PolycyclicRecognition.wordBall_hom_mem_scaled line 48