OAI/Analysis/Kaplansky/Quotient/ClosedStarQuotient.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KaplanskyConsequences.ClosedStarIdeal.submodule line 18
  2. instance OAI.KaplanskyConsequences.ClosedStarIdeal.(instance at line 19) line 19
  3. instance OAI.KaplanskyConsequences.ClosedStarIdeal.(instance at line 20) line 20
  4. def OAI.KaplanskyConsequences.ClosedStarIdeal.ringCon line 22
  5. abbrev OAI.KaplanskyConsequences.ClosedStarIdeal.Quotient line 34
  6. instance OAI.KaplanskyConsequences.ClosedStarIdeal.(instance at line 36) line 36
  7. def OAI.KaplanskyConsequences.ClosedStarIdeal.quotientMap line 38
  8. lemma OAI.KaplanskyConsequences.ClosedStarIdeal.mk_apply line 40
  9. lemma OAI.KaplanskyConsequences.ClosedStarIdeal.mk_surjective line 41
  10. lemma OAI.KaplanskyConsequences.ClosedStarIdeal.mk_eq_zero line 42
  11. instance OAI.KaplanskyConsequences.ClosedStarIdeal.(instance at line 45) line 45
  12. instance OAI.KaplanskyConsequences.ClosedStarIdeal.(instance at line 55) line 55
  13. lemma OAI.KaplanskyConsequences.ClosedStarIdeal.mk_star line 62
  14. instance OAI.KaplanskyConsequences.ClosedStarIdeal.(instance at line 64) line 64
  15. instance OAI.KaplanskyConsequences.ClosedStarIdeal.(instance at line 77) line 77
  16. def OAI.KaplanskyConsequences.ClosedStarIdeal.mkStarAlgHom line 82
  17. lemma OAI.KaplanskyConsequences.ClosedStarIdeal.norm_mk_le line 89
  18. lemma OAI.KaplanskyConsequences.ClosedStarIdeal.norm_mk_lt line 91
  19. instance OAI.KaplanskyConsequences.ClosedStarIdeal.(instance at line 94) line 94
  20. instance OAI.KaplanskyConsequences.ClosedStarIdeal.(instance at line 111) line 111
  21. instance OAI.KaplanskyConsequences.ClosedStarIdeal.(instance at line 114) line 114
  22. lemma OAI.KaplanskyConsequences.ClosedStarIdeal.approximate_unit_mem line 123
  23. lemma OAI.KaplanskyConsequences.ClosedStarIdeal.norm_sq_mk_le_add line 150
  24. instance OAI.KaplanskyConsequences.ClosedStarIdeal.(instance at line 180) line 180
  25. instance OAI.KaplanskyConsequences.ClosedStarIdeal.quotientCStarAlgebra line 195
  26. example OAI.KaplanskyConsequences.ClosedStarIdeal.(example at line 197) line 197