OAI/GroupTheory/PeriodicGroups/Algebra/DirectCancellation.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SourceBurnside.DirectCancellation.eval_ne_zero_nodup line 15
  2. lemma OAI.SourceBurnside.DirectCancellation.interval_eval_ne_zero line 41
  3. def OAI.SourceBurnside.DirectCancellation.EligibleInterval line 49
  4. def OAI.SourceBurnside.DirectCancellation.firstLongRun line 54
  5. lemma OAI.SourceBurnside.DirectCancellation.firstLongRun_spec line 60
  6. lemma OAI.SourceBurnside.DirectCancellation.firstLongRun_first line 67
  7. lemma OAI.SourceBurnside.DirectCancellation.eligibleInterval_uniform line 73
  8. theorem OAI.SourceBurnside.DirectCancellation.direct_cancellation line 87
  9. abbrev OAI.SourceBurnside.Automaton.State line 124
  10. def OAI.SourceBurnside.Automaton.stateCode line 126
  11. lemma OAI.SourceBurnside.Automaton.stateCode_injective line 129
  12. instance OAI.SourceBurnside.Automaton.(instance at line 139) line 139
  13. lemma OAI.SourceBurnside.Automaton.card_state line 141
  14. def OAI.SourceBurnside.Automaton.root line 150
  15. def OAI.SourceBurnside.Automaton.transition line 152
  16. def OAI.SourceBurnside.Automaton.scan line 156
  17. lemma OAI.SourceBurnside.Automaton.transition_mul line 161
  18. theorem OAI.SourceBurnside.Automaton.product_transition line 186
  19. def OAI.SourceBurnside.Automaton.freeScan line 204
  20. lemma OAI.SourceBurnside.Automaton.freeScan_long line 208
  21. lemma OAI.SourceBurnside.Automaton.scan_eq_freeScan line 219
  22. def OAI.SourceBurnside.Automaton.partitions line 230
  23. def OAI.SourceBurnside.Automaton.partitionWeight line 237
  24. lemma OAI.SourceBurnside.Automaton.partitionWeight_empty line 241
  25. lemma OAI.SourceBurnside.Automaton.sum_flatMap line 244
  26. lemma OAI.SourceBurnside.Automaton.freeScan_eq_partitions line 250
  27. theorem OAI.SourceBurnside.Automaton.root_product_eq_partitions line 272
  28. def OAI.SourceBurnside.Automaton.Segments line 282
  29. lemma OAI.SourceBurnside.Automaton.partitions_sound line 285
  30. lemma OAI.SourceBurnside.Automaton.partitions_complete line 317
  31. theorem OAI.SourceBurnside.Automaton.mem_partitions_iff line 355
  32. def OAI.SourceBurnside.Automaton.children line 358
  33. def OAI.SourceBurnside.Automaton.parent line 361
  34. lemma OAI.SourceBurnside.Automaton.parent_children line 367
  35. lemma OAI.SourceBurnside.Automaton.children_nodup line 379
  36. theorem OAI.SourceBurnside.Automaton.partitions_nodup line 387
  37. def OAI.SourceBurnside.Automaton.blockTransition line 407
  38. lemma OAI.SourceBurnside.Automaton.blockTransition_product line 412
  39. theorem OAI.SourceBurnside.Automaton.root_block_eq_partitions line 421
  40. lemma OAI.SourceBurnside.Automaton.card_blockState line 430
  41. def OAI.SourceBurnside.Automaton.combinedWeight line 444
  42. lemma OAI.SourceBurnside.Automaton.combinedWeight_long line 447
  43. lemma OAI.SourceBurnside.Automaton.product_combinedWeight line 458
  44. abbrev OAI.SourceBurnside.Automaton.BoundedSequences line 482
  45. def OAI.SourceBurnside.Automaton.spelled line 484
  46. def OAI.SourceBurnside.Automaton.seqWeight line 487
  47. def OAI.SourceBurnside.Automaton.wordCoefficient line 490
  48. lemma OAI.SourceBurnside.Automaton.length_le_flatten_of_nonempty line 494
  49. lemma OAI.SourceBurnside.Automaton.identifiers_segments line 506
  50. lemma OAI.SourceBurnside.Automaton.bounded_product_combinedWeight line 514
  51. lemma OAI.SourceBurnside.Automaton.spelled_eq_iff_partition line 533
  52. theorem OAI.SourceBurnside.Automaton.wordCoefficient_eq_partitions line 542
  53. theorem OAI.SourceBurnside.Automaton.root_block_eq_wordCoefficient line 576
  54. lemma OAI.SourceBurnside.Automaton.sum_words_eq line 586
  55. theorem OAI.SourceBurnside.Automaton.sum_wordCoefficient line 606