OAI/Analysis/Pureness/Completion/ClosedStarIdealQuotientNorm.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CuntzPureness.ClosedStarIdeal line 12
  2. abbrev OAI.CuntzPureness.ClosedStarIdeal.Quotient line 20
  3. def OAI.CuntzPureness.ClosedStarIdeal.quotientMap line 22
  4. lemma OAI.CuntzPureness.ClosedStarIdeal.quotientMap_surjective line 24
  5. lemma OAI.CuntzPureness.ClosedStarIdeal.rel_star line 27
  6. instance OAI.CuntzPureness.ClosedStarIdeal.quotientStar line 32
  7. lemma OAI.CuntzPureness.ClosedStarIdeal.quotientMap_star line 35
  8. instance OAI.CuntzPureness.ClosedStarIdeal.quotientStarRing line 38
  9. instance OAI.CuntzPureness.ClosedStarIdeal.quotientStarModule line 53
  10. def OAI.CuntzPureness.ClosedStarIdeal.quotientStarHom line 58
  11. abbrev OAI.CuntzPureness.ClosedStarIdeal.idealSubmodule line 61
  12. lemma OAI.CuntzPureness.ClosedStarIdeal.idealSubmodule_coe line 64
  13. instance OAI.CuntzPureness.ClosedStarIdeal.idealSubmodule_closed line 72
  14. def OAI.CuntzPureness.ClosedStarIdeal.quotientLinearEquiv line 76
  15. lemma OAI.CuntzPureness.ClosedStarIdeal.quotientLinearEquiv_mk line 80
  16. instance OAI.CuntzPureness.ClosedStarIdeal.quotientNormedAddCommGroup line 83
  17. instance OAI.CuntzPureness.ClosedStarIdeal.quotientNormedSpace line 87
  18. def OAI.CuntzPureness.ClosedStarIdeal.quotientNormEquiv line 90
  19. lemma OAI.CuntzPureness.ClosedStarIdeal.quotientMap_norm_le line 95
  20. lemma OAI.CuntzPureness.ClosedStarIdeal.quotient_norm_lt_rep line 101
  21. instance OAI.CuntzPureness.ClosedStarIdeal.quotientCompleteSpace line 108
  22. lemma OAI.CuntzPureness.ClosedStarIdeal.quotient_norm_mul_le line 111
  23. instance OAI.CuntzPureness.ClosedStarIdeal.quotientNormedRing line 129
  24. instance OAI.CuntzPureness.ClosedStarIdeal.quotientNormedAlgebra line 133
  25. lemma OAI.CuntzPureness.ClosedStarIdeal.quotient_norm_star line 136
  26. instance OAI.CuntzPureness.ClosedStarIdeal.quotientNormedStarGroup line 145
  27. lemma OAI.CuntzPureness.ClosedStarIdeal.quotientStarHom_continuous line 148