OAI/GroupTheory/SimpleOvergroups/TwoEnlargements.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SourceEnlargement.enlargedGroup line 16
  2. abbrev OAI.SourceEnlargement.enlargedSet line 19
  3. instance OAI.SourceEnlargement.enlargedAction line 21
  4. def OAI.SourceEnlargement.j line 28
  5. def OAI.SourceEnlargement.groupEmbedding line 32
  6. def OAI.SourceEnlargement.pointEmbedding line 35
  7. lemma OAI.SourceEnlargement.groupEmbedding_injective line 37
  8. lemma OAI.SourceEnlargement.pointEmbedding_injective line 43
  9. lemma OAI.SourceEnlargement.groupEmbedding_pointEmbedding line 46
  10. def OAI.SourceEnlargement.pairDiagrams line 52
  11. def OAI.SourceEnlargement.diagramsForward line 63
  12. def OAI.SourceEnlargement.diagramsBackward line 79
  13. def OAI.SourceEnlargement.Saturation.carrier line 94
  14. instance OAI.SourceEnlargement.Saturation.action line 96
  15. def OAI.SourceEnlargement.Saturation.point line 103
  16. lemma OAI.SourceEnlargement.Saturation.point_injective line 105
  17. lemma OAI.SourceEnlargement.Saturation.equivariant line 108
  18. def OAI.SourceEnlargement.Saturation.diagrams line 112
  19. abbrev OAI.SourceEnlargement.Double.W₁ line 125
  20. abbrev OAI.SourceEnlargement.Double.Y₁ line 126
  21. abbrev OAI.SourceEnlargement.Double.W line 127
  22. abbrev OAI.SourceEnlargement.Double.AmbientY line 128
  23. instance OAI.SourceEnlargement.Double.action₁ line 130
  24. instance OAI.SourceEnlargement.Double.action₂ line 133
  25. instance OAI.SourceEnlargement.Double.smul₁ line 136
  26. instance OAI.SourceEnlargement.Double.smul₂ line 137
  27. def OAI.SourceEnlargement.Double.iota line 141
  28. def OAI.SourceEnlargement.Double.ambientPoint line 144
  29. lemma OAI.SourceEnlargement.Double.iota_injective line 147
  30. lemma OAI.SourceEnlargement.Double.ambientPoint_injective line 150
  31. lemma OAI.SourceEnlargement.Double.iota_ambientPoint line 153
  32. def OAI.SourceEnlargement.Double.ambientDiagrams₂ line 160
  33. def OAI.SourceEnlargement.Double.ambientDiagrams₃ line 166
  34. def OAI.SourceEnlargement.Double.orbitSet line 172
  35. abbrev OAI.SourceEnlargement.Double.Y line 175
  36. instance OAI.SourceEnlargement.Double.orbitAction line 177
  37. instance OAI.SourceEnlargement.Double.orbitSMul line 180
  38. def OAI.SourceEnlargement.Double.point line 183
  39. lemma OAI.SourceEnlargement.Double.point_injective line 186
  40. lemma OAI.SourceEnlargement.Double.iota_point line 189
  41. def OAI.SourceEnlargement.Double.diagrams₂ line 193
  42. def OAI.SourceEnlargement.Double.diagrams₃ line 197