OAI/Analysis/PureInfiniteness/CommutativeCoefficientAlgebra.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A finite commuting normal family and its adjoints generate a closed commutative nonunital C*-algebra in the original ambient algebra.

  1. def OAI.WeakPureInfiniteness.coefficientAlgebra line 15
  2. instance OAI.WeakPureInfiniteness.coefficientAlgebra_closed line 18
  3. def OAI.WeakPureInfiniteness.coefficientGenerator line 21
  4. lemma OAI.WeakPureInfiniteness.coefficientAlgebra_commutative line 25