OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanCoverBoxRadius.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Linear metric radius of exponential boxes in the Cartan cover

  1. theorem OAI.PolycyclicRecognition.semidirect_root_generators_linear_metric_bound line 27
  2. theorem OAI.PolycyclicRecognition.exists_semidirect_box_metric_bound line 77