OAI/Geometry/Symplectic/MorseBounds/GroupGap.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArnoldCounterexample.Nondegenerate.GroupGap.coordinate_patterns_injective line 11
2. theorem OAI.ArnoldCounterexample.Nondegenerate.GroupGap.factors_le_card_pow_rank line 36
3. theorem OAI.ArnoldCounterexample.Nondegenerate.GroupGap.group_gap line 43
4. lemma OAI.ArnoldCounterexample.Nondegenerate.GroupGap.card_A5 line 51
5. theorem OAI.ArnoldCounterexample.Nondegenerate.GroupGap.A5_power_rank_gap line 55
6. theorem OAI.ArnoldCounterexample.Nondegenerate.GroupGap.exists_A5_power_rank_gap line 60