OAI/GroupTheory/FiniteType/OrderChainsExactSubtypeOfExactSet.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.OrderChains.exactSubtype_of_exactSet line 12
  2. theorem OAI.TwistedBrin.Basis.CutBasis.localGroup_regular_products line 37
  3. theorem OAI.TwistedBrin.Basis.CutBasis.localGroup_geometric_of_certificates line 66
  4. theorem OAI.SimpleFInftyOvergroups.SplittingTorusModel.finitelyPresented line 92
  5. theorem OAI.SimpleFInftyOvergroups.SplittingTorusModel.productsâ‚‚ line 97
  6. theorem OAI.SimpleFInftyOvergroups.SplittingTorusModel.products line 108
  7. def OAI.TwistedBrin.globalHom line 128
  8. lemma OAI.TwistedBrin.globalHom_injective line 141
  9. lemma OAI.TwistedBrin.pointwise_eq_fixing line 145
  10. lemma OAI.TwistedBrin.pointwise_empty line 152
  11. lemma OAI.TwistedBrin.oligomorphic_of_highly_transitive line 156
  12. theorem OAI.TwistedBrin.localGroup_geometric_of_torus_models line 183
  13. theorem OAI.StageGeometry.localGroup_geometric_of_binary_ring_data line 213
  14. theorem OAI.StageGeometry.localGroup_overgroup_of_binary_ring_data line 236