OAI/Analysis/BoundedHochschild/CStarQuotients.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

C-star quotients by star-closed ideals.

  1. class OAI.HochschildCStarQuotient.StarClosed line 17
  2. lemma OAI.HochschildCStarQuotient.norm_mk_le line 22
  3. lemma OAI.HochschildCStarQuotient.norm_mk_lt line 25
  4. instance OAI.HochschildCStarQuotient.quotientSeminormedRing line 29
  5. instance OAI.HochschildCStarQuotient.quotientNormedRing line 44
  6. instance OAI.HochschildCStarQuotient.quotientNormedAlgebra line 47
  7. instance OAI.HochschildCStarQuotient.quotientStar line 52
  8. lemma OAI.HochschildCStarQuotient.star_mk line 57
  9. instance OAI.HochschildCStarQuotient.quotientStarRing line 59
  10. instance OAI.HochschildCStarQuotient.quotientStarModule line 72
  11. lemma OAI.HochschildCStarQuotient.norm_star_le line 78
  12. instance OAI.HochschildCStarQuotient.quotientNormedStarGroup line 84
  13. def OAI.HochschildCStarQuotient.starSubalgebra line 88
  14. instance OAI.HochschildCStarQuotient.starSubalgebra_closed line 99
  15. lemma OAI.HochschildCStarQuotient.exists_cut line 104
  16. lemma OAI.HochschildCStarQuotient.quotient_cstar line 126
  17. instance OAI.HochschildCStarQuotient.quotientCStarAlgebra line 164