OAI/Analysis/JiangSu/DimensionDrop/ProjectionRanks.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.JiangSuConstruction.matrixTrace line 17
  2. lemma OAI.JiangSuConstruction.matrixTrace_continuous line 21
  3. lemma OAI.JiangSuConstruction.matrixTrace_idempotent line 27
  4. lemma OAI.JiangSuConstruction.matrixTrace_idempotent_zero line 38
  5. lemma OAI.JiangSuConstruction.matrixTrace_idempotent_one line 49
  6. lemma OAI.JiangSuConstruction.matrixTrace_idempotent_path_constant line 60
  7. lemma OAI.JiangSuConstruction.leftAmplification_injective line 85
  8. lemma OAI.JiangSuConstruction.rightAmplification_injective line 94
  9. lemma OAI.JiangSuConstruction.matrixTrace_left line 103
  10. lemma OAI.JiangSuConstruction.matrixTrace_right line 109
  11. theorem OAI.JiangSuConstruction.primeDrop_idempotent_trivial line 118