OAI/GroupTheory/PeriodicGroups/Steinberg/DiagonalActions.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SourceBurnside.Stability.SteinbergAction.scaleHom line 12
2. lemma OAI.SourceBurnside.Stability.SteinbergAction.scaleHom_x line 24
3. lemma OAI.SourceBurnside.Stability.SteinbergAction.scaleHom_one line 28
4. lemma OAI.SourceBurnside.Stability.SteinbergAction.scaleHom_mul line 33
5. def OAI.SourceBurnside.Stability.SteinbergAction.scale line 41
6. lemma OAI.SourceBurnside.Stability.SteinbergAction.scale_apply line 52
7. lemma OAI.SourceBurnside.Stability.SteinbergAction.scale_x line 53
8. lemma OAI.SourceBurnside.Stability.SteinbergAction.scale_inv line 56
9. lemma OAI.SourceBurnside.Stability.SteinbergAction.elementary_eq_e line 60
10. lemma OAI.SourceBurnside.Stability.SteinbergAction.diagonal_conjugate_e line 64
11. lemma OAI.SourceBurnside.Stability.SteinbergAction.representation_scale line 81
12. abbrev OAI.SourceBurnside.Stability.SteinbergAction.GLGenerator line 102
13. def OAI.SourceBurnside.Stability.SteinbergAction.generatorAction line 104
14. def OAI.SourceBurnside.Stability.SteinbergAction.wordAction line 108
15. lemma OAI.SourceBurnside.Stability.SteinbergAction.wordAction_of line 111
16. lemma OAI.SourceBurnside.Stability.SteinbergAction.generator_equivariant line 114
17. lemma OAI.SourceBurnside.Stability.SteinbergAction.word_equivariant line 123
18. def OAI.SourceBurnside.Stability.MatrixK1.E line 155
19. lemma OAI.SourceBurnside.Stability.MatrixK1.elementary_mem line 158
20. lemma OAI.SourceBurnside.Stability.MatrixK1.evaluate_elementary line 161
21. lemma OAI.SourceBurnside.Stability.MatrixK1.normal line 177
22. lemma OAI.SourceBurnside.Stability.MatrixK1.evaluate_mem_iff line 181
23. lemma OAI.SourceBurnside.Stability.MatrixK1.embed_mem line 192
24. lemma OAI.SourceBurnside.Stability.MatrixK1.embed_mem_iff line 201
25. lemma OAI.SourceBurnside.Stability.MatrixK1.coset_representative line 215