OAI/GroupTheory/PolycyclicRecognition/Geometry/CoarsePairHeight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bounded height for uniform families of coarse inverse pairs

Representative existence is proved here from the controlled contraction. The normalized height premise is discharged by the Cartan theorem in the application; it is not declared as a published result.

  1. theorem OAI.PolycyclicRecognition.uniform_affine_height_of_coarse_inverse_pairs line 24