OAI/Geometry/CylinderCovering/Nilpotent/Similarity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CylinderCovering.Nilpotent.sqrtTwo_ne line 11
  2. theorem OAI.CylinderCovering.Nilpotent.sqrtTwo_sq line 12
  3. theorem OAI.CylinderCovering.Nilpotent.centerMap_normalized line 14
  4. theorem OAI.CylinderCovering.Nilpotent.centerMap_uncenterMap line 22
  5. theorem OAI.CylinderCovering.Nilpotent.uncenterMap_centerMap line 27
  6. theorem OAI.CylinderCovering.Nilpotent.centerMap_dist line 31
  7. theorem OAI.CylinderCovering.Nilpotent.centerMap_mem_iff line 38
  8. theorem OAI.CylinderCovering.Nilpotent.centerMap_tetrahedron line 74
  9. theorem OAI.CylinderCovering.Nilpotent.centerMap_area line 83
  10. theorem OAI.CylinderCovering.Nilpotent.centerMap_volume line 104