OAI/GroupTheory/PolycyclicRecognition/Algebra/RiemannianChartLength.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Chart displacement controlled by the length of a path

  1. theorem OAI.PolycyclicRecognition.chart_edist_le_pathELength line 24