OAI/GroupTheory/PolycyclicRecognition/Analysis/CompactSectionVolume.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compact coordinate sections with quantitative retained volume

  1. theorem OAI.PolycyclicRecognition.isCompact_coordinate_section line 16
  2. theorem OAI.PolycyclicRecognition.exists_compact_section_volume_gt line 33