OAI/GroupTheory/PolycyclicRecognition/Algebra/CyclicPingPong.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The cyclic-subgroup form of ping-pong

Only images of the other attracting domains are required here. This form is suited to higher-dimensional projective actions, whose repelling hyperplanes need not be disjoint.

  1. theorem OAI.PolycyclicRecognition.cyclic_ping_pong_injective line 18
  2. theorem OAI.PolycyclicRecognition.polynomial_growth_excludes_cyclic_ping_pong line 44