OAI/GroupTheory/UniversalGroup/MatrixDiagrams.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniversalFInfinity.MatrixDiagram.OrthogonallyAdditive line 22
  2. lemma OAI.UniversalFInfinity.MatrixDiagram.rank_one_idempotent line 26
  3. lemma OAI.UniversalFInfinity.MatrixDiagram.rank_one_mul_zero line 31
  4. lemma OAI.UniversalFInfinity.MatrixDiagram.rank_one_difference line 35
  5. def OAI.UniversalFInfinity.MatrixDiagram.row line 61
  6. def OAI.UniversalFInfinity.MatrixDiagram.along line 62
  7. def OAI.UniversalFInfinity.MatrixDiagram.direction line 63
  8. def OAI.UniversalFInfinity.MatrixDiagram.anchor line 64
  9. def OAI.UniversalFInfinity.MatrixDiagram.witness line 65
  10. lemma OAI.UniversalFInfinity.MatrixDiagram.frame_identities line 67
  11. lemma OAI.UniversalFInfinity.MatrixDiagram.along_step line 75
  12. lemma OAI.UniversalFInfinity.MatrixDiagram.increment_independent line 80
  13. theorem OAI.UniversalFInfinity.MatrixDiagram.prime_multiple_step line 94
  14. lemma OAI.UniversalFInfinity.MatrixDiagram.OrthogonallyAdditive.transpose line 118
  15. lemma OAI.UniversalFInfinity.MatrixDiagram.OrthogonallyAdditive.comp line 131
  16. def OAI.UniversalFInfinity.MatrixDiagram.basisVector line 145
  17. def OAI.UniversalFInfinity.MatrixDiagram.diagonalUnit line 147
  18. theorem OAI.UniversalFInfinity.MatrixDiagram.diagonal_zero_one line 150
  19. lemma OAI.UniversalFInfinity.MatrixDiagram.reindex_diagonalUnit line 182
  20. theorem OAI.UniversalFInfinity.MatrixDiagram.diagonal_equality line 194
  21. lemma OAI.UniversalFInfinity.MatrixDiagram.diagonalUnit_idempotent line 214
  22. lemma OAI.UniversalFInfinity.MatrixDiagram.diagonalUnit_orthogonal line 219
  23. lemma OAI.UniversalFInfinity.MatrixDiagram.diagonalUnit_sum line 224
  24. abbrev OAI.UniversalFInfinity.PrefixAlgebra.Sequences line 235
  25. abbrev OAI.UniversalFInfinity.PrefixAlgebra.Space line 236
  26. abbrev OAI.UniversalFInfinity.PrefixAlgebra.Operators line 237
  27. def OAI.UniversalFInfinity.PrefixAlgebra.prefixOp line 239
  28. def OAI.UniversalFInfinity.PrefixAlgebra.delete line 242
  29. lemma OAI.UniversalFInfinity.PrefixAlgebra.prefix_single line 245
  30. lemma OAI.UniversalFInfinity.PrefixAlgebra.delete_single line 249
  31. lemma OAI.UniversalFInfinity.PrefixAlgebra.delete_prefix line 253
  32. lemma OAI.UniversalFInfinity.PrefixAlgebra.prefix_partition line 263
  33. def OAI.UniversalFInfinity.PrefixAlgebra.algebra line 270
  34. def OAI.UniversalFInfinity.PrefixAlgebra.left line 273
  35. def OAI.UniversalFInfinity.PrefixAlgebra.right line 275
  36. lemma OAI.UniversalFInfinity.PrefixAlgebra.right_left line 278
  37. lemma OAI.UniversalFInfinity.PrefixAlgebra.partition line 283
  38. def OAI.UniversalFInfinity.PrefixAlgebra.leftWord line 287
  39. def OAI.UniversalFInfinity.PrefixAlgebra.rightWord line 291
  40. lemma OAI.UniversalFInfinity.PrefixAlgebra.leftWord_nil line 295
  41. lemma OAI.UniversalFInfinity.PrefixAlgebra.rightWord_nil line 296
  42. lemma OAI.UniversalFInfinity.PrefixAlgebra.cancel_initial line 298
  43. lemma OAI.UniversalFInfinity.PrefixAlgebra.word_cancel line 305
  44. def OAI.UniversalFInfinity.PrefixAlgebra.words line 310
  45. lemma OAI.UniversalFInfinity.PrefixAlgebra.word_orthogonality line 315
  46. def OAI.UniversalFInfinity.PrefixAlgebra.projection line 320
  47. lemma OAI.UniversalFInfinity.PrefixAlgebra.projection_idempotent line 322
  48. lemma OAI.UniversalFInfinity.PrefixAlgebra.projection_split line 327
  49. abbrev OAI.UniversalFInfinity.MatrixCorners.unit line 351
  50. lemma OAI.UniversalFInfinity.MatrixCorners.unit_mul line 356
  51. lemma OAI.UniversalFInfinity.MatrixCorners.weighted_unit_mul line 363
  52. def OAI.UniversalFInfinity.MatrixCorners.matrixMap line 369
  53. lemma OAI.UniversalFInfinity.MatrixCorners.matrixMap_mul line 372
  54. def OAI.UniversalFInfinity.MatrixCorners.hom line 391
  55. lemma OAI.UniversalFInfinity.MatrixCorners.map_diagonal line 398
  56. lemma OAI.UniversalFInfinity.MatrixCorners.map_one line 403
  57. lemma OAI.UniversalFInfinity.MatrixCorners.extract line 407