OAI/GroupTheory/PolycyclicRecognition/Algebra/LeftInvariantRiemannianLength.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Left translation preserves the Riemannian length

  1. abbrev OAI.PolycyclicRecognition.leftRiemannianBundle line 18
  2. theorem OAI.PolycyclicRecognition.leftRiemannian_inner line 21
  3. theorem OAI.PolycyclicRecognition.norm_mfderiv_leftTranslation line 25
  4. theorem OAI.PolycyclicRecognition.pathELength_leftTranslation line 34
  5. theorem OAI.PolycyclicRecognition.riemannianEDist_leftTranslation line 61