OAI/GroupTheory/PolycyclicRecognition/Analysis/TemplateSupportOrder.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.SupportDatum.weightSupport_eq_of_bound_and_attained line 19
2. theorem OAI.PolycyclicRecognition.SupportDatum.weightSupport_mono line 31
3. theorem OAI.PolycyclicRecognition.SupportDatum.templateSupport_lt_of_weightSupport line 41

   Source documentation

   Every word basis contains every generator with positive multiplicity, so decreasing one support strictly decreases the entire finite maximum.

   theorem templateSupport_lt_of_weightSupport {E F : Set W}
       (hle : ∀ i, D.weightSupport E i ≤ D.weightSupport F i)
       (hlt : ∃ i, D.weightSupport E i < D.weightSupport F i) :
       D.templateSupport E < D.templateSupport F := by
   …