OAI/GroupTheory/SimpleOvergroups/ContractedNormalForms.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SimpleFInftyOvergroups.SemanticEncoding.NormalPresentation line 14
  2. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.NormalPresentation.q_normal line 28
  3. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.NormalPresentation.normal_eq_zero_iff line 31
  4. def OAI.SimpleFInftyOvergroups.SemanticEncoding.NormalPresentation.representative line 34
  5. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.NormalPresentation.representative_q line 36
  6. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.NormalPresentation.q_representative line 40
  7. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.NormalPresentation.representative_injective line 43
  8. def OAI.SimpleFInftyOvergroups.SemanticEncoding.NormalPresentation.algebraMap line 47
  9. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.NormalPresentation.algebraMap_single line 50
  10. def OAI.SimpleFInftyOvergroups.SemanticEncoding.NormalPresentation.sectionMap line 54
  11. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.NormalPresentation.sectionMap_basis line 58
  12. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.NormalPresentation.algebraMap_section line 73
  13. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.NormalPresentation.sectionMap_injective line 83
  14. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.NormalPresentation.algebraMap_surjective line 86
  15. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.NormalPresentation.section_algebraMap_single line 89
  16. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.NormalPresentation.section_algebraMap line 94
  17. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.NormalPresentation.algebraMap_eq_iff_collect line 102