OAI/GroupTheory/PeriodicGroups/Matrices/ElementaryGenerators.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceBurnside.Stability.MatrixGenerators.elementary line 13
  2. lemma OAI.SourceBurnside.Stability.MatrixGenerators.elementary_val line 19
  3. def OAI.SourceBurnside.Stability.MatrixGenerators.diagonal line 22
  4. lemma OAI.SourceBurnside.Stability.MatrixGenerators.diagonal_val line 32
  5. lemma OAI.SourceBurnside.Stability.MatrixGenerators.diagonal_one line 35
  6. lemma OAI.SourceBurnside.Stability.MatrixGenerators.diagonal_mul line 39
  7. def OAI.SourceBurnside.Stability.MatrixGenerators.singleDiagonal line 43
  8. def OAI.SourceBurnside.Stability.MatrixGenerators.generated line 46
  9. lemma OAI.SourceBurnside.Stability.MatrixGenerators.elementary_mem line 49
  10. lemma OAI.SourceBurnside.Stability.MatrixGenerators.singleDiagonal_mem line 52
  11. lemma OAI.SourceBurnside.Stability.MatrixGenerators.diagonal_mem line 55
  12. def OAI.SourceBurnside.Stability.MatrixGenerators.relabel line 72
  13. lemma OAI.SourceBurnside.Stability.MatrixGenerators.relabel_elementary line 75
  14. lemma OAI.SourceBurnside.Stability.MatrixGenerators.relabel_diagonal line 82
  15. lemma OAI.SourceBurnside.Stability.MatrixGenerators.relabel_singleDiagonal line 87
  16. lemma OAI.SourceBurnside.Stability.MatrixGenerators.relabel_mem line 94
  17. def OAI.SourceBurnside.Stability.MatrixGenerators.blockInclusion line 107
  18. lemma OAI.SourceBurnside.Stability.MatrixGenerators.blockInclusion_val line 116
  19. lemma OAI.SourceBurnside.Stability.MatrixGenerators.blockInclusion_elementary line 119
  20. lemma OAI.SourceBurnside.Stability.MatrixGenerators.blockInclusion_diagonal line 127
  21. lemma OAI.SourceBurnside.Stability.MatrixGenerators.blockInclusion_mem line 133
  22. def OAI.SourceBurnside.Stability.MatrixGenerators.column line 147
  23. def OAI.SourceBurnside.Stability.MatrixGenerators.row line 148
  24. def OAI.SourceBurnside.Stability.MatrixGenerators.scalarOne line 149
  25. def OAI.SourceBurnside.Stability.MatrixGenerators.upperStrip line 151
  26. lemma OAI.SourceBurnside.Stability.MatrixGenerators.upperStrip_val line 157
  27. lemma OAI.SourceBurnside.Stability.MatrixGenerators.upperStrip_zero line 161
  28. lemma OAI.SourceBurnside.Stability.MatrixGenerators.upperStrip_add line 165
  29. lemma OAI.SourceBurnside.Stability.MatrixGenerators.upperStrip_single line 173
  30. lemma OAI.SourceBurnside.Stability.MatrixGenerators.upperStrip_mem line 181
  31. def OAI.SourceBurnside.Stability.MatrixGenerators.lowerStrip line 196
  32. lemma OAI.SourceBurnside.Stability.MatrixGenerators.lowerStrip_val line 202
  33. lemma OAI.SourceBurnside.Stability.MatrixGenerators.lowerStrip_zero line 206
  34. lemma OAI.SourceBurnside.Stability.MatrixGenerators.lowerStrip_add line 210
  35. lemma OAI.SourceBurnside.Stability.MatrixGenerators.lowerStrip_single line 216
  36. lemma OAI.SourceBurnside.Stability.MatrixGenerators.lowerStrip_mem line 224
  37. lemma OAI.SourceBurnside.Stability.MatrixGenerators.block_diagonal_val line 239
  38. lemma OAI.SourceBurnside.Stability.MatrixGenerators.schur_factorization line 251
  39. lemma OAI.SourceBurnside.Stability.LinearAlgebra.matrix_nil line 292
  40. lemma OAI.SourceBurnside.Stability.LinearAlgebra.nil_of_reduce_zero line 299
  41. lemma OAI.SourceBurnside.Stability.LinearAlgebra.isUnit_of_reduce_one line 307
  42. lemma OAI.SourceBurnside.Stability.LinearAlgebra.isUnit_iff_reduce_ne_zero line 311
  43. lemma OAI.SourceBurnside.Stability.LinearAlgebra.isUnit_matrix_of_reduce_one line 321
  44. theorem OAI.SourceBurnside.Stability.LinearAlgebra.isUnit_matrix_iff line 330
  45. lemma OAI.SourceBurnside.Stability.LinearAlgebra.relabel_reduce_one line 351
  46. lemma OAI.SourceBurnside.Stability.LinearAlgebra.relabel_symm_apply line 359
  47. lemma OAI.SourceBurnside.Stability.LinearAlgebra.identity_residue_generated line 365
  48. lemma OAI.SourceBurnside.Stability.LinearAlgebra.representation_mem_generated line 407
  49. theorem OAI.SourceBurnside.Stability.LinearAlgebra.full_matrix_generated line 419
  50. theorem OAI.SourceBurnside.Stability.LinearAlgebra.all_matrix_generated line 440