OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanUniformBridgeGeometry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Thickened bridge bounds with a preassigned smallness threshold

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.assemble_uniform_bridge_point line 36
  2. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_uniform_thickened_bridge_lifts line 91