OAI/GroupTheory/PeriodicGroups/Frames/ElementaryFrames.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SourceBurnside.Stability.MatrixK1.representation_range line 14
2. lemma OAI.SourceBurnside.Stability.MatrixK1.permutation_mem line 32
3. lemma OAI.SourceBurnside.Stability.MatrixK1.embed_sumInl line 45
4. lemma OAI.SourceBurnside.Stability.MatrixK1.block_mem line 66
5. lemma OAI.SourceBurnside.Stability.MatrixK1.rectangle_mem line 77
6. lemma OAI.SourceBurnside.Stability.MatrixK1.block_smul_right line 81
7. lemma OAI.SourceBurnside.Stability.MatrixK1.block_mem_iff line 92
8. lemma OAI.SourceBurnside.Stability.MatrixK1.ordered_transitive line 99
9. lemma OAI.SourceBurnside.Stability.ColumnRelabel.relabel_elementary_mem line 128
10. def OAI.SourceBurnside.Stability.ColumnRelabel.elementaryEquiv line 137
11. def OAI.SourceBurnside.Stability.ColumnRelabel.coordinateEquiv line 144
12. def OAI.SourceBurnside.Stability.ColumnRelabel.vertexEquiv line 152
13. lemma OAI.SourceBurnside.Stability.ColumnRelabel.rho_vertex line 169
14. lemma OAI.SourceBurnside.Stability.ColumnRelabel.independent line 173
15. lemma OAI.SourceBurnside.Stability.ColumnRelabel.independent_symm line 183
16. lemma OAI.SourceBurnside.Stability.ColumnRelabel.vertex_action line 188
17. lemma OAI.SourceBurnside.Stability.ColumnRelabel.independent_action line 196
18. def OAI.SourceBurnside.Stability.ColumnRelabel.homologyIso line 203