OAI/GroupTheory/PeriodicGroups/Presentation/FinitePresentation.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SourceBurnside.Stability.LinearAlgebra.extend_independent_map line 11
2. theorem OAI.SourceBurnside.Stability.LinearAlgebra.complete_columns line 25
3. inductive OAI.SourceBurnside.Stability.SmallPresentation.Generator line 69
4. def OAI.SourceBurnside.Stability.SmallPresentation.Generator.support line 75
5. def OAI.SourceBurnside.Stability.SmallPresentation.Generator.map line 79
6. def OAI.SourceBurnside.Stability.SmallPresentation.Generator.matrix line 84
7. def OAI.SourceBurnside.Stability.SmallPresentation.matrixWord line 91
8. def OAI.SourceBurnside.Stability.SmallPresentation.supported line 94
9. def OAI.SourceBurnside.Stability.SmallPresentation.relations line 97
10. abbrev OAI.SourceBurnside.Stability.SmallPresentation.Group line 100
11. def OAI.SourceBurnside.Stability.SmallPresentation.evaluate line 102
12. def OAI.SourceBurnside.Stability.SmallPresentation.gen line 105
13. lemma OAI.SourceBurnside.Stability.SmallPresentation.evaluate_gen line 107
14. lemma OAI.SourceBurnside.Stability.SmallPresentation.evaluate_surjective line 110
15. lemma OAI.SourceBurnside.Stability.SmallPresentation.supported_univ line 122
16. theorem OAI.SourceBurnside.Stability.SmallPresentation.evaluate_injective_small line 126
17. def OAI.SourceBurnside.Stability.MatrixGenerators.embeddingEquiv line 147
18. lemma OAI.SourceBurnside.Stability.MatrixGenerators.embeddingEquiv_inl line 152
19. lemma OAI.SourceBurnside.Stability.MatrixGenerators.embeddingEquiv_inr line 154
20. def OAI.SourceBurnside.Stability.MatrixGenerators.embed line 157
21. lemma OAI.SourceBurnside.Stability.MatrixGenerators.embed_elementary line 160
22. lemma OAI.SourceBurnside.Stability.MatrixGenerators.blockInclusion_singleDiagonal line 165
23. lemma OAI.SourceBurnside.Stability.MatrixGenerators.embed_singleDiagonal line 172
24. lemma OAI.SourceBurnside.Stability.MatrixGenerators.embed_entry line 177
25. lemma OAI.SourceBurnside.Stability.MatrixGenerators.embed_injective line 185
26. lemma OAI.SourceBurnside.Stability.MatrixGenerators.embed_off_column line 191
27. lemma OAI.SourceBurnside.Stability.MatrixGenerators.embed_off_row line 207
28. lemma OAI.SourceBurnside.Stability.SmallPresentation.generator_map_matrix line 233
29. lemma OAI.SourceBurnside.Stability.SmallPresentation.matrixWord_map line 237
30. lemma OAI.SourceBurnside.Stability.SmallPresentation.supported_map line 244
31. def OAI.SourceBurnside.Stability.SmallPresentation.inclusion line 264
32. lemma OAI.SourceBurnside.Stability.SmallPresentation.inclusion_gen line 273
33. lemma OAI.SourceBurnside.Stability.SmallPresentation.evaluate_inclusion line 279
34. lemma OAI.SourceBurnside.Stability.SmallPresentation.evaluate_inclusion_apply line 285
35. lemma OAI.SourceBurnside.Stability.SmallPresentation.supported_letter line 289
36. lemma OAI.SourceBurnside.Stability.SmallPresentation.local_equality line 292
37. lemma OAI.SourceBurnside.Stability.SmallPresentation.small_eval_injective line 299
38. def OAI.SourceBurnside.Stability.SmallPresentation.localGroup line 319
39. lemma OAI.SourceBurnside.Stability.SmallPresentation.gen_mem_local line 322
40. lemma OAI.SourceBurnside.Stability.SmallPresentation.localGroup_mono line 325
41. lemma OAI.SourceBurnside.Stability.SmallPresentation.evaluate_mk line 332
42. lemma OAI.SourceBurnside.Stability.SmallPresentation.local_faithful line 335
43. lemma OAI.SourceBurnside.Stability.SmallPresentation.localGroup_eq_closure line 342
44. lemma OAI.SourceBurnside.Stability.SmallPresentation.range_inclusion line 349
45. lemma OAI.SourceBurnside.Stability.SmallPresentation.supported_gen_all line 378
46. def OAI.SourceBurnside.Stability.SmallPresentation.root line 392
47. def OAI.SourceBurnside.Stability.SmallPresentation.diag line 393
48. lemma OAI.SourceBurnside.Stability.SmallPresentation.evaluate_root line 395
49. lemma OAI.SourceBurnside.Stability.SmallPresentation.evaluate_diag line 397
50. lemma OAI.SourceBurnside.Stability.SmallPresentation.root_mem_local line 400
51. lemma OAI.SourceBurnside.Stability.SmallPresentation.diag_mem_local line 403
52. lemma OAI.SourceBurnside.Stability.SmallPresentation.root_add line 406
53. lemma OAI.SourceBurnside.Stability.SmallPresentation.root_zero line 415
54. lemma OAI.SourceBurnside.Stability.SmallPresentation.root_neg line 420
55. lemma OAI.SourceBurnside.Stability.SmallPresentation.root_commute line 424
56. lemma OAI.SourceBurnside.Stability.SmallPresentation.diag_inv line 444
57. def OAI.SourceBurnside.Stability.SmallPresentation.rowHom line 452
58. lemma OAI.SourceBurnside.Stability.SmallPresentation.rowHom_single line 459
59. def OAI.SourceBurnside.Stability.SmallPresentation.rowGroup line 463
60. lemma OAI.SourceBurnside.Stability.SmallPresentation.root_mem_row line 465
61. lemma OAI.SourceBurnside.Stability.SmallPresentation.row_mem line 479
62. lemma OAI.SourceBurnside.Stability.SmallPresentation.rowGroup_le line 489
63. def OAI.SourceBurnside.Stability.SmallPresentation.rowMatrix line 494
64. lemma OAI.SourceBurnside.Stability.SmallPresentation.rowMatrix_entry line 498
65. lemma OAI.SourceBurnside.Stability.SmallPresentation.rowMatrix_product line 502
66. lemma OAI.SourceBurnside.Stability.SmallPresentation.rowMatrix_one line 511
67. lemma OAI.SourceBurnside.Stability.SmallPresentation.rowMatrix_mul line 515
68. def OAI.SourceBurnside.Stability.SmallPresentation.rowUnits line 521
69. lemma OAI.SourceBurnside.Stability.SmallPresentation.rowMatrix_single line 534
70. lemma OAI.SourceBurnside.Stability.SmallPresentation.rowUnits_single line 549
71. lemma OAI.SourceBurnside.Stability.SmallPresentation.evaluate_rowHom line 555
72. lemma OAI.SourceBurnside.Stability.SmallPresentation.evaluate_rowHom_apply line 562
73. lemma OAI.SourceBurnside.Stability.SmallPresentation.rowUnits_injective line 565
74. lemma OAI.SourceBurnside.Stability.SmallPresentation.row_faithful line 572