OAI/GroupTheory/FiniteType/SourceEnlargement.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceEnlargement.D₂ line 11
  2. def OAI.SourceEnlargement.D₃ line 12
  3. instance OAI.SourceEnlargement.(instance at line 13) line 13
  4. instance OAI.SourceEnlargement.(instance at line 14) line 14
  5. instance OAI.SourceEnlargement.(instance at line 15) line 15
  6. instance OAI.SourceEnlargement.(instance at line 17) line 17
  7. instance OAI.SourceEnlargement.(instance at line 19) line 19
  8. instance OAI.SourceEnlargement.(instance at line 21) line 21
  9. def OAI.SourceEnlargement.P₂ line 23
  10. def OAI.SourceEnlargement.P₃ line 24
  11. lemma OAI.SourceEnlargement.idempotent₂ line 26
  12. lemma OAI.SourceEnlargement.idempotent₃ line 28
  13. def OAI.SourceEnlargement.I₂ line 31
  14. def OAI.SourceEnlargement.I₃ line 32
  15. def OAI.SourceEnlargement.W₁ line 34
  16. instance OAI.SourceEnlargement.(instance at line 36) line 36
  17. def OAI.SourceEnlargement.Y₁ line 38
  18. def OAI.SourceEnlargement.W line 39
  19. instance OAI.SourceEnlargement.(instance at line 41) line 41
  20. def OAI.SourceEnlargement.Y₂ line 43
  21. instance OAI.SourceEnlargement.layer₁Action line 45
  22. instance OAI.SourceEnlargement.layer₂Action line 49
  23. abbrev OAI.SourceEnlargement.j₂ line 53
  24. abbrev OAI.SourceEnlargement.j₃ line 55
  25. def OAI.SourceEnlargement.iota line 58
  26. def OAI.SourceEnlargement.point₁ line 60
  27. def OAI.SourceEnlargement.point₂ line 62
  28. def OAI.SourceEnlargement.family₂ line 65
  29. def OAI.SourceEnlargement.family₃ line 67
  30. lemma OAI.SourceEnlargement.iota_injective line 75
  31. lemma OAI.SourceEnlargement.point₁_injective line 79
  32. lemma OAI.SourceEnlargement.point₂_injective line 81
  33. lemma OAI.SourceEnlargement.point₁_equivariant line 84
  34. lemma OAI.SourceEnlargement.point₂_equivariant line 88
  35. lemma OAI.SourceEnlargement.family₂_identity line 94
  36. lemma OAI.SourceEnlargement.family₃_identity line 95
  37. lemma OAI.SourceEnlargement.family₂_commute line 97
  38. lemma OAI.SourceEnlargement.family₃_commute line 103
  39. lemma OAI.SourceEnlargement.family₂_addition line 109
  40. lemma OAI.SourceEnlargement.family₃_addition line 116
  41. lemma OAI.SourceEnlargement.family₂_fixed line 122
  42. lemma OAI.SourceEnlargement.family₃_fixed line 129
  43. def OAI.SourceEnlargement.orbitPoints line 134
  44. abbrev OAI.SourceEnlargement.Y line 135
  45. instance OAI.SourceEnlargement.orbitAction line 137
  46. lemma OAI.SourceEnlargement.orbit_smul_val line 144
  47. def OAI.SourceEnlargement.point line 147
  48. lemma OAI.SourceEnlargement.point_val line 149
  49. lemma OAI.SourceEnlargement.point_injective line 151
  50. lemma OAI.SourceEnlargement.point_equivariant line 155
  51. def OAI.SourceEnlargement.diagram₂ line 160
  52. def OAI.SourceEnlargement.diagram₃ line 167
  53. theorem OAI.SourceEnlargement.overgroup_of_corner_data line 182