OAI/GroupTheory/PeriodicGroups/Presentation/SmallFaithful.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.SourceBurnside.Stability.SmallPresentation.columnAction line 14
2. lemma OAI.SourceBurnside.Stability.SmallPresentation.column_smul line 17
3. lemma OAI.SourceBurnside.Stability.SmallPresentation.parabolic_fix line 20
4. lemma OAI.SourceBurnside.Stability.SmallPresentation.swap_smul line 25
5. def OAI.SourceBurnside.Stability.SmallPresentation.cosetData line 31
6. lemma OAI.SourceBurnside.Stability.SmallPresentation.evaluate_injective_step line 73
7. theorem OAI.SourceBurnside.Stability.SmallPresentation.evaluate_injective line 106
8. def OAI.SourceBurnside.Stability.SmallPresentation.equivalence line 124
9. lemma OAI.SourceBurnside.Stability.SmallPresentation.equivalence_apply line 128
10. def OAI.SourceBurnside.Stability.SmallPresentation.elementaryGroup line 143
11. lemma OAI.SourceBurnside.Stability.SmallPresentation.root_mem_elementary line 146
12. lemma OAI.SourceBurnside.Stability.SmallPresentation.diag_normalizes_elementary line 149
13. instance OAI.SourceBurnside.Stability.SmallPresentation.elementary_normal line 169
14. abbrev OAI.SourceBurnside.Stability.SmallPresentation.K1 line 179
15. def OAI.SourceBurnside.Stability.SmallPresentation.toK1 line 181
16. lemma OAI.SourceBurnside.Stability.SmallPresentation.toK1_root line 184
17. lemma OAI.SourceBurnside.Stability.SmallPresentation.diag_one line 187
18. lemma OAI.SourceBurnside.Stability.SmallPresentation.minus_one_unit line 194
19. lemma OAI.SourceBurnside.Stability.SmallPresentation.toK1_swap line 200
20. lemma OAI.SourceBurnside.Stability.SmallPresentation.toK1_diag_eq line 203
21. lemma OAI.SourceBurnside.Stability.SmallPresentation.elementary_inclusion line 212
22. def OAI.SourceBurnside.Stability.SmallPresentation.K1map line 221
23. lemma OAI.SourceBurnside.Stability.SmallPresentation.K1map_mk line 225
24. lemma OAI.SourceBurnside.Stability.SmallPresentation.supported_range line 229
25. def OAI.SourceBurnside.Stability.SmallPresentation.unitWord line 245
26. lemma OAI.SourceBurnside.Stability.SmallPresentation.unitWord_map line 250
27. lemma OAI.SourceBurnside.Stability.SmallPresentation.unitWord_relation line 264
28. def OAI.SourceBurnside.Stability.SmallPresentation.collapseGroup line 287
29. lemma OAI.SourceBurnside.Stability.SmallPresentation.collapseGroup_root line 291
30. lemma OAI.SourceBurnside.Stability.SmallPresentation.collapseGroup_diag line 295
31. lemma OAI.SourceBurnside.Stability.SmallPresentation.collapseGroup_kills line 299
32. def OAI.SourceBurnside.Stability.SmallPresentation.collapse line 305
33. lemma OAI.SourceBurnside.Stability.SmallPresentation.collapse_mk line 309
34. lemma OAI.SourceBurnside.Stability.SmallPresentation.collapse_left line 312
35. lemma OAI.SourceBurnside.Stability.SmallPresentation.collapse_right line 328
36. def OAI.SourceBurnside.Stability.SmallPresentation.K1equivalence line 345