OAI/RepresentationTheory/FoulkesSixth/SemisimpleBridge.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Foulkes.SemisimpleBridge.homCongrRight line 17
  2. lemma OAI.Foulkes.SemisimpleBridge.finite_hom line 27
  3. lemma OAI.Foulkes.SemisimpleBridge.simple_hom_finrank line 32
  4. def OAI.Foulkes.SemisimpleBridge.fibreEmbedding line 58
  5. lemma OAI.Foulkes.SemisimpleBridge.fibreEmbedding_label line 68
  6. lemma OAI.Foulkes.SemisimpleBridge.hom_pi_finrank line 85
  7. def OAI.Foulkes.SemisimpleBridge.piMapOfMatching line 100
  8. lemma OAI.Foulkes.SemisimpleBridge.piMapOfMatching_apply line 106
  9. lemma OAI.Foulkes.SemisimpleBridge.piMapOfMatching_injective line 119
  10. def OAI.Foulkes.SemisimpleBridge.classSet line 133
  11. lemma OAI.Foulkes.SemisimpleBridge.classSet_eq_iff line 135
  12. theorem OAI.Foulkes.SemisimpleBridge.matching_of_equivalence_counts line 146
  13. def OAI.Foulkes.SemisimpleBridge.moduleIsoSetoid line 171
  14. theorem OAI.Foulkes.SemisimpleBridge.pi_embedding_of_iso_counts line 176
  15. theorem OAI.Foulkes.SemisimpleBridge.embedding_of_simple_hom_le line 194