OAI/GroupTheory/PeriodicGroups/Steinberg/RankActions.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SourceBurnside.Stability.ElementaryRanks.Group line 12
  2. def OAI.SourceBurnside.Stability.ElementaryRanks.representation line 14
  3. lemma OAI.SourceBurnside.Stability.ElementaryRanks.representation_val line 20
  4. lemma OAI.SourceBurnside.Stability.ElementaryRanks.representation_surjective line 23
  5. def OAI.SourceBurnside.Stability.ElementaryRanks.root line 30
  6. lemma OAI.SourceBurnside.Stability.ElementaryRanks.root_val line 31
  7. lemma OAI.SourceBurnside.Stability.ElementaryRanks.rep_kernel line 35
  8. def OAI.SourceBurnside.Stability.ElementaryRanks.next line 43
  9. lemma OAI.SourceBurnside.Stability.ElementaryRanks.next_root line 48
  10. lemma OAI.SourceBurnside.Stability.ElementaryRanks.next_representation line 56
  11. lemma OAI.SourceBurnside.Stability.ElementaryRanks.next_h2_isIso line 62
  12. lemma OAI.SourceBurnside.Stability.FiniteRootPairs.finite_pair line 79
  13. lemma OAI.SourceBurnside.Stability.FiniteRootPairs.finite_pair_commute line 116
  14. def OAI.SourceBurnside.Stability.RationalExtension.finiteOrderLift line 127
  15. lemma OAI.SourceBurnside.Stability.RationalExtension.finiteOrderLift_projection line 131
  16. lemma OAI.SourceBurnside.Stability.RationalExtension.finiteOrderLift_torsion line 134
  17. lemma OAI.SourceBurnside.Stability.ExtensionRootLift.add_self_zero line 143
  18. lemma OAI.SourceBurnside.Stability.ExtensionRootLift.x_sq line 149
  19. lemma OAI.SourceBurnside.Stability.ExtensionRootLift.root_sq line 151
  20. lemma OAI.SourceBurnside.Stability.ExtensionRootLift.root_torsion line 153
  21. lemma OAI.SourceBurnside.Stability.ExtensionRootLift.root_add line 156
  22. lemma OAI.SourceBurnside.Stability.ExtensionRootLift.root_commute line 159
  23. lemma OAI.SourceBurnside.Stability.ExtensionRootLift.root_same_commute line 162
  24. lemma OAI.SourceBurnside.Stability.ExtensionRootLift.root_mul line 166
  25. lemma OAI.SourceBurnside.Stability.ExtensionRootLift.consecutive_finite line 170
  26. lemma OAI.SourceBurnside.Stability.ExtensionRootLift.unique_over line 182
  27. def OAI.SourceBurnside.Stability.ExtensionRootLift.lift line 193
  28. lemma OAI.SourceBurnside.Stability.ExtensionRootLift.projection_lift line 194
  29. lemma OAI.SourceBurnside.Stability.ExtensionRootLift.lift_torsion line 196
  30. lemma OAI.SourceBurnside.Stability.ExtensionRootLift.lift_eq_finite line 198
  31. lemma OAI.SourceBurnside.Stability.ExtensionRootLift.lift_add line 203
  32. lemma OAI.SourceBurnside.Stability.ExtensionRootLift.lift_commute line 213
  33. lemma OAI.SourceBurnside.Stability.ExtensionRootLift.lift_mul line 223
  34. def OAI.SourceBurnside.Stability.ExtensionRootLift.hom line 236
  35. lemma OAI.SourceBurnside.Stability.ExtensionRootLift.hom_x line 237
  36. lemma OAI.SourceBurnside.Stability.ExtensionRootLift.hom_projection line 238
  37. lemma OAI.SourceBurnside.Stability.ExtensionRootLift.hom_unique line 244
  38. def OAI.SourceBurnside.Stability.SteinbergAction.preservers line 261
  39. lemma OAI.SourceBurnside.Stability.SteinbergAction.scale_strip line 271
  40. lemma OAI.SourceBurnside.Stability.SteinbergAction.scale_preserves_strip line 281
  41. lemma OAI.SourceBurnside.Stability.SteinbergAction.conj_preserves_column line 292
  42. lemma OAI.SourceBurnside.Stability.SteinbergAction.conj_preserves_row line 299
  43. lemma OAI.SourceBurnside.Stability.SteinbergAction.fixes_strip line 306
  44. lemma OAI.SourceBurnside.Stability.SteinbergAction.identity_of_fixes_strips line 314
  45. lemma OAI.SourceBurnside.Stability.SteinbergAction.supported_column line 344
  46. lemma OAI.SourceBurnside.Stability.SteinbergAction.supported_row line 356
  47. lemma OAI.SourceBurnside.Stability.SteinbergAction.supported_relation_trivial line 368
  48. lemma OAI.SourceBurnside.Stability.SteinbergAction.small_relation_trivial line 380
  49. def OAI.SourceBurnside.Stability.SteinbergAction.presentationAction line 387
  50. lemma OAI.SourceBurnside.Stability.SteinbergAction.presentationAction_gen line 390
  51. def OAI.SourceBurnside.Stability.SteinbergAction.matrixAction line 399
  52. lemma OAI.SourceBurnside.Stability.SteinbergAction.matrixAction_e line 402
  53. lemma OAI.SourceBurnside.Stability.SteinbergAction.matrixAction_representation line 413
  54. theorem OAI.SourceBurnside.Stability.SteinbergAction.kernel_central line 421
  55. theorem OAI.SourceBurnside.ConcreteSource.kernel_central line 439
  56. theorem OAI.SourceBurnside.ConcreteSource.kernel_central_rank line 443