OAI/Analysis/JiangSu/DimensionDrop/DimensionDropSquare.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.MatrixTensor.matrixSubalgebraClosed line 15
  2. instance OAI.MatrixTensor.matrixSubalgebraCStar line 17
  3. def OAI.MatrixTensor.fiberMap line 26
  4. def OAI.MatrixTensor.fiberAlgebra line 31
  5. lemma OAI.MatrixTensor.mul_mem_fiber line 34
  6. lemma OAI.MatrixTensor.fiber_finite_sum line 39
  7. def OAI.JiangSuConstruction.dropFiber line 59
  8. lemma OAI.JiangSuConstruction.drop_mem_fiber line 63
  9. def OAI.JiangSuConstruction.squareSections line 70
  10. instance OAI.JiangSuConstruction.squareSections_closed line 80
  11. abbrev OAI.JiangSuConstruction.Square line 89
  12. lemma OAI.JiangSuConstruction.sectionMap_mem_square line 91
  13. def OAI.JiangSuConstruction.squareTensorMap line 102
  14. theorem OAI.JiangSuConstruction.squareTensorMap_injective line 111