OAI/GroupTheory/SimpleOvergroups/CodeEmbedding.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeTable.table_short line 16
2. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeTable.canonical_no_infix line 24
3. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeTable.canonical_irreducible line 49
4. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeTable.output_eq_iff line 60
5. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.Families.table_short line 87
6. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.Families.isolate line 95
7. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeQuotient.normal_encode line 130
8. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeQuotient.present_encode_iff line 147
9. def OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeQuotient.codeHom line 161
10. def OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeQuotient.descendCode line 170
11. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeQuotient.descendCode_apply line 184
12. theorem OAI.SimpleFInftyOvergroups.ContextualEncoding.CodeQuotient.descendCode_injective line 189