OAI/GroupTheory/PeriodicGroups/Homology/LocallyFiniteActions.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SourceBurnside.Stability.LocallyFinite.finite line 12
2. lemma OAI.SourceBurnside.Stability.LocallyFinite.of_injective line 16
3. lemma OAI.SourceBurnside.Stability.LocallyFinite.of_surjective line 25
4. lemma OAI.SourceBurnside.Stability.LocallyFinite.commTorsion line 38
5. lemma OAI.SourceBurnside.Stability.LocallyFinite.vector2 line 49
6. abbrev OAI.SourceBurnside.Stability.UnorderedStabilizer.rightVertex line 70
7. lemma OAI.SourceBurnside.Stability.UnorderedStabilizer.rightVertex_injective line 73
8. abbrev OAI.SourceBurnside.Stability.UnorderedStabilizer.K line 76
9. def OAI.SourceBurnside.Stability.UnorderedStabilizer.rightEquiv line 79
10. def OAI.SourceBurnside.Stability.UnorderedStabilizer.perm line 82
11. lemma OAI.SourceBurnside.Stability.UnorderedStabilizer.perm_spec line 89
12. def OAI.SourceBurnside.Stability.UnorderedStabilizer.permRight line 94
13. lemma OAI.SourceBurnside.Stability.UnorderedStabilizer.permRight_eq line 98
14. lemma OAI.SourceBurnside.Stability.UnorderedStabilizer.permRight_smul line 101
15. def OAI.SourceBurnside.Stability.UnorderedStabilizer.fixedPart line 108
16. def OAI.SourceBurnside.Stability.UnorderedStabilizer.topBlock line 117
17. lemma OAI.SourceBurnside.Stability.UnorderedStabilizer.topBlock_entry line 120
18. lemma OAI.SourceBurnside.Stability.UnorderedStabilizer.shape line 126
19. def OAI.SourceBurnside.Stability.UnorderedStabilizer.projectionGL line 143
20. lemma OAI.SourceBurnside.Stability.UnorderedStabilizer.topBlock_mem line 160
21. def OAI.SourceBurnside.Stability.UnorderedStabilizer.projection line 167
22. def OAI.SourceBurnside.Stability.UnorderedStabilizer.quotientMap line 170
23. lemma OAI.SourceBurnside.Stability.UnorderedStabilizer.section_mem line 173
24. def OAI.SourceBurnside.Stability.UnorderedStabilizer.sectionElement line 194
25. lemma OAI.SourceBurnside.Stability.UnorderedStabilizer.section_perm line 198
26. lemma OAI.SourceBurnside.Stability.UnorderedStabilizer.section_topBlock line 208
27. lemma OAI.SourceBurnside.Stability.UnorderedStabilizer.quotientMap_surjective line 217
28. lemma OAI.SourceBurnside.Stability.UnorderedStabilizer.kernel_shape line 224
29. def OAI.SourceBurnside.Stability.UnorderedStabilizer.strip line 233
30. lemma OAI.SourceBurnside.Stability.UnorderedStabilizer.strip_injective line 246
31. lemma OAI.SourceBurnside.Stability.UnorderedStabilizer.kernel_locallyFinite line 256
32. lemma OAI.SourceBurnside.Stability.Frames.labelMap_basis_congr line 265
33. lemma OAI.SourceBurnside.Stability.Frames.labelMap_basis_fixed line 274
34. lemma OAI.SourceBurnside.Stability.Frames.labelMap_basis_swap line 279
35. lemma OAI.SourceBurnside.Stability.Frames.labelMap_basis_transposition line 292
36. abbrev OAI.SourceBurnside.Stability.MonomialInduction.charRep line 318
37. lemma OAI.SourceBurnside.Stability.MonomialInduction.charRep_apply line 323
38. lemma OAI.SourceBurnside.Stability.MonomialInduction.ind_relation line 326
39. def OAI.SourceBurnside.Stability.MonomialInduction.basisSeed line 337
40. def OAI.SourceBurnside.Stability.MonomialInduction.induced line 347
41. lemma OAI.SourceBurnside.Stability.MonomialInduction.induced_mk line 350
42. def OAI.SourceBurnside.Stability.MonomialInduction.transporter line 358
43. lemma OAI.SourceBurnside.Stability.MonomialInduction.transporter_spec line 359
44. def OAI.SourceBurnside.Stability.MonomialInduction.coefficient line 361
45. def OAI.SourceBurnside.Stability.MonomialInduction.orbitBasis line 363
46. lemma OAI.SourceBurnside.Stability.MonomialInduction.orbitBasis_eq line 365
47. def OAI.SourceBurnside.Stability.MonomialInduction.inverseLinear line 372
48. lemma OAI.SourceBurnside.Stability.MonomialInduction.inverseLinear_basis line 376
49. lemma OAI.SourceBurnside.Stability.MonomialInduction.induced_inverse line 381
50. def OAI.SourceBurnside.Stability.MonomialInduction.residual line 389
51. lemma OAI.SourceBurnside.Stability.MonomialInduction.action_residual line 395
52. lemma OAI.SourceBurnside.Stability.MonomialInduction.inverse_induced line 405
53. lemma OAI.SourceBurnside.Stability.MonomialInduction.induced_isIso line 426
54. def OAI.SourceBurnside.Stability.MonomialInduction.scalar line 444
55. lemma OAI.SourceBurnside.Stability.MonomialInduction.scalar_spec line 446
56. lemma OAI.SourceBurnside.Stability.MonomialInduction.smul_basis_injective line 453
57. def OAI.SourceBurnside.Stability.MonomialInduction.character line 458
58. lemma OAI.SourceBurnside.Stability.MonomialInduction.character_spec line 477
59. lemma OAI.SourceBurnside.Stability.MonomialInduction.character_eq_one line 480
60. lemma OAI.SourceBurnside.Stability.MonomialInduction.character_eq_neg_one line 487
61. def OAI.SourceBurnside.Stability.ShapiroMap.resolution line 502
62. lemma OAI.SourceBurnside.Stability.ShapiroMap.comparison_π line 505
63. def OAI.SourceBurnside.Stability.ShapiroMap.comparisonTensor line 514
64. lemma OAI.SourceBurnside.Stability.ShapiroMap.comparison_homology_isIso line 519
65. def OAI.SourceBurnside.Stability.ShapiroMap.tensorIso line 536
66. def OAI.SourceBurnside.Stability.ShapiroMap.unit line 541
67. lemma OAI.SourceBurnside.Stability.ShapiroMap.unit_apply line 544
68. lemma OAI.SourceBurnside.Stability.ShapiroMap.tensorIso_mk line 547
69. lemma OAI.SourceBurnside.Stability.ShapiroMap.chain_compare line 554
70. lemma OAI.SourceBurnside.Stability.ShapiroMap.map_isIso line 574