OAI/GroupTheory/FiniteType/HomStabilizer.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HomStabilizer.conjugateTuple line 11
  2. def OAI.HomStabilizer.enumeratedSubset line 30
  3. structure OAI.SimpleFInftyOvergroups.SplittingTorusModel line 46
  4. def OAI.SimpleFInftyOvergroups.SplittingTorusModel.relabel line 65
  5. theorem OAI.SimpleFInftyOvergroups.SplittingTorusModel.geometric line 68
  6. theorem OAI.SimpleFInftyOvergroups.SplittingTorusModel.setwise_geometric line 73
  7. theorem OAI.StageGeometry.finite_tuple_model line 98
  8. theorem OAI.StageGeometry.finite_tuple_geometric line 137
  9. abbrev OAI.StageGeometry.limitAction line 162
  10. theorem OAI.StageGeometry.finite_set_model line 166
  11. theorem OAI.StageGeometry.finite_setwise_geometric line 190
  12. theorem OAI.StageGeometry.finite_pointwise_geometric line 201
  13. theorem OAI.StageGeometry.limit_geometric line 213
  14. theorem OAI.StageGeometry.all_geometric_of_ring_data line 223