OAI/GroupTheory/CyclicSeries/Length.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

Cyclic subnormal series and their minimum lengths in finite p-groups.

  1. structure OAI.ChromaticCyclic.CyclicStep line 9

    Also declared: ComparatorChallenges/PolycyclicRecognition.lean:16 (same declaration text).

  2. structure OAI.ChromaticCyclic.CyclicSeries line 14

    Also declared: ComparatorChallenges/PolycyclicRecognition.lean:21 (same declaration text).

  3. def OAI.ChromaticCyclic.cyclicLength line 20
  4. abbrev OAI.ChromaticCyclic.CyclicPower line 23
  5. theorem OAI.ChromaticCyclic.CyclicStep.normal_map line 28
  6. def OAI.ChromaticCyclic.CyclicStep.factorMap line 35
  7. theorem OAI.ChromaticCyclic.CyclicStep.factorMap_surjective line 45
  8. theorem OAI.ChromaticCyclic.CyclicStep.map line 54
  9. theorem OAI.ChromaticCyclic.CyclicStep.normal_comap line 62
  10. def OAI.ChromaticCyclic.CyclicStep.factorComap line 69
  11. theorem OAI.ChromaticCyclic.CyclicStep.factorComap_injective line 78
  12. theorem OAI.ChromaticCyclic.CyclicStep.comap line 93
  13. theorem OAI.ChromaticCyclic.cyclic_pGroup_disjoint line 103
  14. theorem OAI.ChromaticCyclic.CyclicStep.factorMap_injective_of_stable line 145
  15. theorem OAI.ChromaticCyclic.CyclicStep.refl line 187
  16. theorem OAI.ChromaticCyclic.CyclicStep.bot line 195
  17. def OAI.ChromaticCyclic.CyclicSeries.refl line 204
  18. def OAI.ChromaticCyclic.CyclicSeries.cons line 210
  19. def OAI.ChromaticCyclic.CyclicSeries.map line 219
  20. def OAI.ChromaticCyclic.CyclicSeries.comap line 226
  21. def OAI.ChromaticCyclic.CyclicSeries.tail line 233
  22. theorem OAI.ChromaticCyclic.CyclicSeries.le line 239
  23. theorem OAI.ChromaticCyclic.CyclicStep.exists_larger line 250
  24. theorem OAI.ChromaticCyclic.CyclicSeries.pad line 275
  25. def OAI.ChromaticCyclic.CyclicSeries.changes line 282
  26. def OAI.ChromaticCyclic.CyclicSeries.repetitions line 286
  27. theorem OAI.ChromaticCyclic.CyclicSeries.changes_add_repetitions line 290
  28. theorem OAI.ChromaticCyclic.CyclicSeries.compressed line 296
  29. theorem OAI.ChromaticCyclic.CyclicSeries.exists_of_normalizerCondition line 315
  30. theorem OAI.ChromaticCyclic.CyclicSeries.exists_of_pGroup line 326
  31. theorem OAI.ChromaticCyclic.cyclicLength_le line 333
  32. theorem OAI.ChromaticCyclic.cyclicLength_le_changes line 336
  33. theorem OAI.ChromaticCyclic.cyclicLength_le_iff line 341
  34. theorem OAI.ChromaticCyclic.CyclicStep.relIndex_dvd_of_pow line 355
  35. theorem OAI.ChromaticCyclic.CyclicStep.relIndex_eq_of_stable line 367
  36. theorem OAI.ChromaticCyclic.CyclicSeries.prod_relIndex line 383
  37. theorem OAI.ChromaticCyclic.CyclicSeries.prod_relIndex_bot_top line 400
  38. theorem OAI.ChromaticCyclic.CyclicSeries.card_growth line 405
  39. instance OAI.ChromaticCyclic.CyclicPower.finite line 437
  40. theorem OAI.ChromaticCyclic.CyclicPower.card line 441
  41. theorem OAI.ChromaticCyclic.CyclicPower.pow_power line 444
  42. def OAI.ChromaticCyclic.CyclicPower.reduction line 451
  43. theorem OAI.ChromaticCyclic.CyclicPower.reduction_surjective line 457
  44. theorem OAI.ChromaticCyclic.CyclicPower.reduction_comp line 465
  45. def OAI.ChromaticCyclic.ProductTower.reduction line 477
  46. theorem OAI.ChromaticCyclic.ProductTower.reduction_surjective line 481
  47. theorem OAI.ChromaticCyclic.ProductTower.reduction_comp line 487
  48. theorem OAI.ChromaticCyclic.ProductTower.reduction_inl line 493
  49. theorem OAI.ChromaticCyclic.ProductTower.pow_power line 500
  50. theorem OAI.ChromaticCyclic.ProductTower.isPGroup line 508
  51. def OAI.ChromaticCyclic.CyclicSeries.mapSurjective line 519
  52. def OAI.ChromaticCyclic.CyclicSeries.comapInjective line 526
  53. theorem OAI.ChromaticCyclic.product_series line 537
  54. def OAI.ChromaticCyclic.CyclicSeries.append line 619
  55. theorem OAI.ChromaticCyclic.CyclicSeries.nonempty_zero_iff line 631
  56. theorem OAI.ChromaticCyclic.cyclicLength_spec line 642
  57. theorem OAI.ChromaticCyclic.cyclicLength_top line 647
  58. theorem OAI.ChromaticCyclic.cyclicLength_eq_zero_iff line 650
  59. theorem OAI.ChromaticCyclic.cyclicLength_pos_iff line 660
  60. theorem OAI.ChromaticCyclic.cyclicLength_map_le line 665
  61. theorem OAI.ChromaticCyclic.cyclicLength_comap_le line 674
  62. theorem OAI.ChromaticCyclic.cyclicLength_comap_surjective line 682
  63. theorem OAI.ChromaticCyclic.cyclicLength_normal_quotient line 691
  64. theorem OAI.ChromaticCyclic.cyclicLength_map_equiv line 698
  65. theorem OAI.ChromaticCyclic.cyclicLength_conj line 706
  66. theorem OAI.ChromaticCyclic.cyclicLength_triangle line 711