OAI/Analysis/JiangSu/CentralSequences/NormCentralSequenceAlgebra.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NonunitalGamma.normCentralizer line 20
  2. lemma OAI.NonunitalGamma.mem_normCentralizer line 34
  3. lemma OAI.NonunitalGamma.normCentralizer_closed line 38
  4. instance OAI.NonunitalGamma.(instance at line 43) line 43
  5. instance OAI.NonunitalGamma.(instance at line 44) line 44
  6. instance OAI.NonunitalGamma.(instance at line 46) line 46
  7. instance OAI.NonunitalGamma.(instance at line 47) line 47
  8. instance OAI.NonunitalGamma.(instance at line 48) line 48
  9. instance OAI.NonunitalGamma.(instance at line 49) line 49
  10. def OAI.NonunitalGamma.normCentralInclusion line 51
  11. def OAI.NonunitalGamma.normAnnihilator line 59
  12. abbrev OAI.NonunitalGamma.CentralSequenceAlgebra line 100
  13. def OAI.NonunitalGamma.centralSequenceQuotient line 102
  14. def OAI.NonunitalGamma.centralLocalUnit line 108
  15. lemma OAI.NonunitalGamma.centralLocalUnit_mul line 113
  16. lemma OAI.NonunitalGamma.mul_centralLocalUnit line 116
  17. instance OAI.NonunitalGamma.(instance at line 120) line 120
  18. lemma OAI.NonunitalGamma.centralSequence_one_mul line 122
  19. lemma OAI.NonunitalGamma.centralSequence_mul_one line 132
  20. instance OAI.NonunitalGamma.(instance at line 142) line 142
  21. instance OAI.NonunitalGamma.(instance at line 146) line 146
  22. instance OAI.NonunitalGamma.(instance at line 154) line 154
  23. instance OAI.NonunitalGamma.(instance at line 156) line 156
  24. instance OAI.NonunitalGamma.(instance at line 159) line 159
  25. instance OAI.NonunitalGamma.(instance at line 161) line 161
  26. instance OAI.NonunitalGamma.(instance at line 163) line 163
  27. instance OAI.NonunitalGamma.(instance at line 164) line 164
  28. def OAI.NonunitalGamma.centralSequenceToTracialNonunital line 188
  29. lemma OAI.NonunitalGamma.centralSequenceToTracialNonunital_mk line 212
  30. lemma OAI.NonunitalGamma.centralSequenceToTracialNonunital_one line 215
  31. def OAI.NonunitalGamma.centralSequenceToTracial line 222
  32. lemma OAI.NonunitalGamma.centralSequenceToTracial_mk line 233
  33. lemma OAI.NonunitalGamma.centralSequenceToTracial_commutes line 236
  34. theorem OAI.NonunitalGamma.centralSequenceToTracial_range line 243