OAI/GroupTheory/PeriodicGroups/Presentation/SmallSwapActions.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SourceBurnside.Stability.SmallPresentation.card_quad_le line 15
  2. lemma OAI.SourceBurnside.Stability.SmallPresentation.swap_inv line 22
  3. lemma OAI.SourceBurnside.Stability.SmallPresentation.swap_conjugate_root line 25
  4. lemma OAI.SourceBurnside.Stability.SmallPresentation.swap_conjugate_diag line 38
  5. lemma OAI.SourceBurnside.Stability.SmallPresentation.swap_mem_parabolic line 49
  6. lemma OAI.SourceBurnside.Stability.SmallPresentation.parabolic_swap_generates line 56
  7. def OAI.SourceBurnside.Stability.SmallPresentation.fixingGroup line 87
  8. lemma OAI.SourceBurnside.Stability.SmallPresentation.fixingGroup_le_parabolic line 90
  9. lemma OAI.SourceBurnside.Stability.SmallPresentation.evaluate_fixingGroup line 96
  10. lemma OAI.SourceBurnside.Stability.SmallPresentation.swap_conjugate_fixingGroup_le line 112
  11. lemma OAI.SourceBurnside.Stability.SmallPresentation.swap_normalizes_double_fixer line 129
  12. def OAI.SourceBurnside.Stability.FrameTransport.Edge line 153
  13. lemma OAI.SourceBurnside.Stability.FrameTransport.Edge.symm line 155
  14. lemma OAI.SourceBurnside.Stability.FrameTransport.edge_outside line 158
  15. lemma OAI.SourceBurnside.Stability.FrameTransport.edge_to_cone line 167
  16. lemma OAI.SourceBurnside.Stability.FrameTransport.triangle_to_cone line 171
  17. structure OAI.SourceBurnside.Stability.FrameTransport.FlatSystem line 189
  18. def OAI.SourceBurnside.Stability.FrameTransport.connector line 200
  19. lemma OAI.SourceBurnside.Stability.FrameTransport.connector_outside line 202
  20. lemma OAI.SourceBurnside.Stability.FrameTransport.base_connector line 209
  21. lemma OAI.SourceBurnside.Stability.FrameTransport.vertex_connector line 212
  22. def OAI.SourceBurnside.Stability.FrameTransport.canonical line 217
  23. lemma OAI.SourceBurnside.Stability.FrameTransport.canonical_base line 221
  24. lemma OAI.SourceBurnside.Stability.FrameTransport.canonical_to_cone line 224
  25. theorem OAI.SourceBurnside.Stability.FrameTransport.canonical_edge line 239
  26. theorem OAI.SourceBurnside.Stability.FrameTransport.unique_section line 266
  27. def OAI.SourceBurnside.Stability.ColumnFrames.residue line 290
  28. def OAI.SourceBurnside.Stability.ColumnFrames.Vertex line 291
  29. def OAI.SourceBurnside.Stability.ColumnFrames.rho line 292
  30. def OAI.SourceBurnside.Stability.ColumnFrames.standard line 294
  31. lemma OAI.SourceBurnside.Stability.ColumnFrames.rho_standard line 297
  32. lemma OAI.SourceBurnside.Stability.ColumnFrames.standard_injective line 301
  33. lemma OAI.SourceBurnside.Stability.ColumnFrames.rho_spanning line 306
  34. def OAI.SourceBurnside.Stability.ColumnFrames.cones line 313
  35. def OAI.SourceBurnside.Stability.ColumnFrames.reduce line 317
  36. lemma OAI.SourceBurnside.Stability.ColumnFrames.residue_smul line 319
  37. instance OAI.SourceBurnside.Stability.ColumnFrames.(instance at line 325) line 325
  38. lemma OAI.SourceBurnside.Stability.ColumnFrames.smul_val line 333
  39. lemma OAI.SourceBurnside.Stability.ColumnFrames.rho_smul line 334
  40. lemma OAI.SourceBurnside.Stability.ColumnFrames.independent_map line 337
  41. lemma OAI.SourceBurnside.Stability.ColumnFrames.edge_map line 346
  42. lemma OAI.SourceBurnside.Stability.ColumnFrames.triangle_map line 351
  43. lemma OAI.SourceBurnside.Stability.ColumnFrames.standard_independent line 356
  44. lemma OAI.SourceBurnside.Stability.ColumnFrames.standard_edge line 361
  45. lemma OAI.SourceBurnside.Stability.ColumnFrames.standard_triangle line 365
  46. lemma OAI.SourceBurnside.Stability.ColumnFrames.permutation_standard line 369
  47. lemma OAI.SourceBurnside.Stability.ColumnFrames.complete line 374
  48. lemma OAI.SourceBurnside.Stability.ColumnFrames.mem_fixer_iff_standard line 397
  49. lemma OAI.SourceBurnside.Stability.ColumnFrames.pair_injective line 406
  50. lemma OAI.SourceBurnside.Stability.ColumnFrames.triple_injective line 410
  51. lemma OAI.SourceBurnside.Stability.ColumnFrames.edge_transitive line 415
  52. lemma OAI.SourceBurnside.Stability.ColumnFrames.triangle_transitive line 432
  53. structure OAI.SourceBurnside.Stability.CosetTransport.Data line 464
  54. def OAI.SourceBurnside.Stability.CosetTransport.point line 490
  55. lemma OAI.SourceBurnside.Stability.CosetTransport.point_mk line 496
  56. def OAI.SourceBurnside.Stability.CosetTransport.Fiber line 498
  57. def OAI.SourceBurnside.Stability.CosetTransport.Arrow line 500
  58. lemma OAI.SourceBurnside.Stability.CosetTransport.arrow_reverse line 503
  59. lemma OAI.SourceBurnside.Stability.CosetTransport.arrow_edge line 508
  60. lemma OAI.SourceBurnside.Stability.CosetTransport.arrow_unique line 513
  61. lemma OAI.SourceBurnside.Stability.CosetTransport.arrow_exists line 524
  62. lemma OAI.SourceBurnside.Stability.CosetTransport.arrow_triangle line 537
  63. def OAI.SourceBurnside.Stability.CosetTransport.next line 571
  64. lemma OAI.SourceBurnside.Stability.CosetTransport.next_arrow line 574
  65. lemma OAI.SourceBurnside.Stability.CosetTransport.next_eq line 577
  66. lemma OAI.SourceBurnside.Stability.CosetTransport.next_reverse line 582
  67. def OAI.SourceBurnside.Stability.CosetTransport.system line 586
  68. theorem OAI.SourceBurnside.Stability.CosetTransport.point_injective line 603