OAI/Analysis/IrrationalRotation/Operators/TowerBlockAlgebras.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Invariant233.TowerMatrixUnits.IsBlockMatrixUnitFamily line 11
  2. def OAI.Invariant233.TowerMatrixUnits.blockMatrixGenerators line 15
  3. theorem OAI.Invariant233.TowerMatrixUnits.blockMatrixUnit_mem_span line 19
  4. theorem OAI.Invariant233.TowerMatrixUnits.blockMatrixGenerators_mul line 24
  5. theorem OAI.Invariant233.TowerMatrixUnits.blockMatrixGenerators_star line 43
  6. def OAI.Invariant233.TowerMatrixUnits.blockMatrixAlgebra line 52
  7. theorem OAI.Invariant233.TowerMatrixUnits.blockMatrixAlgebra_finiteDimensional line 57
  8. theorem OAI.Invariant233.TowerMatrixUnits.blockMatrixUnit_mem_blockMatrixAlgebra line 62
  9. theorem OAI.Invariant233.TowerMatrixUnits.blockMatrixAlgebra_le line 67
  10. theorem OAI.Invariant233.TowerMatrixUnits.blockMatrixAlgebra_eq_adjoin line 75
  11. theorem OAI.Invariant233.TowerMatrixUnits.compressed_cross_eq_zero line 88
  12. theorem OAI.Invariant233.TowerMatrixUnits.towerEntry_cross_eq_zero line 99
  13. theorem OAI.Invariant233.TowerMatrixUnits.towerEntry_isBlockMatrixUnitFamily line 111
  14. theorem OAI.Invariant233.TowerMatrixUnits.exists_finiteDimensional_blockTowerAlgebra line 123