OAI/Analysis/Nuclearity/DenseUnitalCompletion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The image of the algebraic unit is the unit in a dense C*-completion.

  1. lemma OAI.WeakPureInfiniteness.dense_unit_mul line 12
  2. lemma OAI.WeakPureInfiniteness.dense_mul_unit line 18
  3. abbrev OAI.WeakPureInfiniteness.denseUnitalCStarAlgebra line 24
  4. lemma OAI.WeakPureInfiniteness.denseUnitalCStarAlgebra_one line 28
  5. def OAI.WeakPureInfiniteness.denseUnitalHom line 34