OAI/RingTheory/BassTrace/CentralizerGeometry.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BassTrace.Detector.SubtypeCentralizer_commutes line 16
  2. abbrev OAI.BassTrace.Detector.Centralizer line 19
  3. def OAI.BassTrace.Detector.generator line 21
  4. lemma OAI.BassTrace.Detector.generator_coe line 24
  5. lemma OAI.BassTrace.Detector.generator_commutes line 26
  6. def OAI.BassTrace.Detector.cyclic line 30
  7. instance OAI.BassTrace.Detector.cyclic_normal line 32
  8. abbrev OAI.BassTrace.Detector.ActingGroup line 39
  9. def OAI.BassTrace.Detector.centralizerPerm line 41
  10. lemma OAI.BassTrace.Detector.cyclic_le_ker line 50
  11. def OAI.BassTrace.Detector.quotientPerm line 61
  12. instance OAI.BassTrace.Detector.vertexAction line 64
  13. lemma OAI.BassTrace.Detector.quotient_smul_project line 67
  14. lemma OAI.BassTrace.Detector.vertex_action_free line 70
  15. lemma OAI.BassTrace.Detector.actingGroup_injective_orbit line 88
  16. def OAI.BassTrace.Detector.rightMul line 101
  17. lemma OAI.BassTrace.Detector.rightMul_project line 109
  18. lemma OAI.BassTrace.Detector.rightMul_one line 111
  19. lemma OAI.BassTrace.Detector.rightMul_mul line 116
  20. lemma OAI.BassTrace.Detector.smul_rightMul line 122
  21. def OAI.BassTrace.Detector.supportGraph line 129
  22. lemma OAI.BassTrace.Detector.supportGraph_adj line 137
  23. lemma OAI.BassTrace.Detector.supportGraph_smul line 140
  24. lemma OAI.BassTrace.Detector.supportGraph_finite_neighbors line 150
  25. lemma OAI.BassTrace.Detector.supportGraph_degree_le line 163
  26. lemma OAI.BassTrace.Detector.supportGraph_reachable_rightMul line 173
  27. lemma OAI.BassTrace.Detector.supportGraph_connected line 192