OAI/GroupTheory/PolycyclicRecognition/Geometry/IntrinsicCartanHeightAssembly.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The uniform height theorem with intrinsic Cartan factors

The factors, coordinates, realization, ergodic decomposition, reduced cohomology, and polynomial and metric estimates are supplied by proved constructions for the actual unimodular group.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_uniform_height_intrinsic line 37