OAI/GroupTheory/PolycyclicRecognition/Algebra/ChamberExtremeDirections.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Extreme directions span a full-dimensional weight chamber

  1. def OAI.PolycyclicRecognition.chamberExtremeDirections line 15
  2. theorem OAI.PolycyclicRecognition.extremePoint_base_extreme_ray line 18
  3. theorem OAI.PolycyclicRecognition.chamberBase_subset_span_extremeDirections line 70
  4. theorem OAI.PolycyclicRecognition.closedChamber_subset_span_extremeDirections line 81
  5. theorem OAI.PolycyclicRecognition.span_chamberExtremeDirections_eq_top line 95