OAI/GroupTheory/PolycyclicRecognition/Algebra/SmallEigenlineCones.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Small cones around different lines are disjoint

  1. theorem OAI.PolycyclicRecognition.exists_positive_interval_lt line 14
  2. theorem OAI.PolycyclicRecognition.small_eigenline_cones_disjoint line 23