OAI/GroupTheory/PeriodicGroups/Presentation/MatrixStabilizers.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SourceBurnside.Stability.MatrixGenerators.rectangleLower line 12
2. lemma OAI.SourceBurnside.Stability.MatrixGenerators.rectangleLower_single line 34
3. lemma OAI.SourceBurnside.Stability.MatrixGenerators.rectangleLower_mem line 44
4. def OAI.SourceBurnside.Stability.MatrixGenerators.rightFixer line 55
5. lemma OAI.SourceBurnside.Stability.MatrixGenerators.mem_rightFixer_iff line 58
6. lemma OAI.SourceBurnside.Stability.MatrixGenerators.rightFixer_shape line 70
7. def OAI.SourceBurnside.Stability.MatrixGenerators.rightProjection line 80
8. lemma OAI.SourceBurnside.Stability.MatrixGenerators.rightFixer_decomposition line 106
9. lemma OAI.SourceBurnside.Stability.MatrixGenerators.block_mem_of_generators line 116
10. lemma OAI.SourceBurnside.Stability.MatrixGenerators.rightFixer_generated line 132
11. def OAI.SourceBurnside.Stability.MatrixGenerators.fixer line 143
12. lemma OAI.SourceBurnside.Stability.MatrixGenerators.mem_fixer_iff line 146
13. def OAI.SourceBurnside.Stability.MatrixGenerators.splitEquiv line 158
14. lemma OAI.SourceBurnside.Stability.MatrixGenerators.splitEquiv_inl line 162
15. lemma OAI.SourceBurnside.Stability.MatrixGenerators.splitEquiv_inr line 164
16. lemma OAI.SourceBurnside.Stability.MatrixGenerators.relabel_fixer_right line 166
17. lemma OAI.SourceBurnside.Stability.MatrixGenerators.fixer_generated line 178
18. lemma OAI.SourceBurnside.Stability.MatrixGenerators.elementary_mem_fixer line 200
19. lemma OAI.SourceBurnside.Stability.MatrixGenerators.singleDiagonal_mem_fixer line 207
20. lemma OAI.SourceBurnside.Stability.SmallPresentation.card_triple_le line 228
21. lemma OAI.SourceBurnside.Stability.SmallPresentation.root_conjugate_reverse line 234
22. lemma OAI.SourceBurnside.Stability.SmallPresentation.root_conjugate_row_mem line 251
23. lemma OAI.SourceBurnside.Stability.SmallPresentation.diag_conjugate_root_matrix line 261
24. lemma OAI.SourceBurnside.Stability.SmallPresentation.diag_conjugate_root line 282
25. lemma OAI.SourceBurnside.Stability.SmallPresentation.root_normalizes_row line 293
26. lemma OAI.SourceBurnside.Stability.SmallPresentation.diag_normalizes_row line 308
27. def OAI.SourceBurnside.Stability.SmallPresentation.complementary line 325
28. def OAI.SourceBurnside.Stability.SmallPresentation.parabolic line 326
29. lemma OAI.SourceBurnside.Stability.SmallPresentation.complementary_normalizes_row line 328
30. lemma OAI.SourceBurnside.Stability.SmallPresentation.parabolic_decomposition line 341
31. lemma OAI.SourceBurnside.Stability.SmallPresentation.embedded_row_eq_one line 361
32. lemma OAI.SourceBurnside.Stability.SmallPresentation.root_mem_parabolic line 388
33. lemma OAI.SourceBurnside.Stability.SmallPresentation.diag_mem_parabolic line 396
34. lemma OAI.SourceBurnside.Stability.SmallPresentation.parabolic_le line 400
35. lemma OAI.SourceBurnside.Stability.SmallPresentation.evaluate_parabolic_le line 415
36. lemma OAI.SourceBurnside.Stability.SmallPresentation.evaluate_parabolic line 427
37. lemma OAI.SourceBurnside.Stability.SmallPresentation.parabolic_product_kernel line 436
38. lemma OAI.SourceBurnside.Stability.SmallPresentation.parabolic_kernel_trivial line 450
39. lemma OAI.SourceBurnside.Stability.SmallPresentation.parabolic_faithful line 459
40. def OAI.SourceBurnside.Stability.MatrixGenerators.permutation line 477
41. lemma OAI.SourceBurnside.Stability.MatrixGenerators.permutation_val line 479
42. lemma OAI.SourceBurnside.Stability.MatrixGenerators.permutation_entry line 482
43. lemma OAI.SourceBurnside.Stability.MatrixGenerators.permutation_mul line 488
44. lemma OAI.SourceBurnside.Stability.MatrixGenerators.mul_permutation line 492
45. lemma OAI.SourceBurnside.Stability.MatrixGenerators.permutation_conjugate line 496
46. lemma OAI.SourceBurnside.Stability.MatrixGenerators.permutation_conjugate_elementary line 502
47. lemma OAI.SourceBurnside.Stability.MatrixGenerators.permutation_conjugate_diagonal line 507
48. lemma OAI.SourceBurnside.Stability.MatrixGenerators.permutation_smul line 511
49. lemma OAI.SourceBurnside.Stability.MatrixGenerators.permutation_smul_single line 524
50. def OAI.SourceBurnside.Stability.SmallPresentation.swap line 541
51. lemma OAI.SourceBurnside.Stability.SmallPresentation.swap_mem_local line 544
52. lemma OAI.SourceBurnside.Stability.SmallPresentation.evaluate_swap line 550
53. lemma OAI.SourceBurnside.Stability.SmallPresentation.swap_square line 564
54. lemma OAI.SourceBurnside.Stability.SmallPresentation.swap_braid line 570