OAI/Analysis/JiangSu/DimensionDrop/PermutationUnitary.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.JiangSuConstruction.zeroReducedEquiv line 14
  2. def OAI.JiangSuConstruction.zeroTensorEquiv line 17
  3. def OAI.JiangSuConstruction.oneReducedEquiv line 19
  4. def OAI.JiangSuConstruction.oneTensorEquiv line 22
  5. def OAI.JiangSuConstruction.zeroIndexEquiv line 25
  6. def OAI.JiangSuConstruction.oneIndexEquiv line 29
  7. lemma OAI.JiangSuConstruction.zeroIndex_endpoint line 34
  8. lemma OAI.JiangSuConstruction.oneIndex_endpoint line 66
  9. def OAI.JiangSuConstruction.concreteStep line 98
  10. theorem OAI.JiangSuConstruction.concreteStep_injective line 106