OAI/Analysis/OperatorAlgebra/CyclicCoefficientApproximation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite cyclic-vector approximation in KR02 Lemma 7.18. The cyclic representation is on the unitization, so this applies to nonunital algebras without assuming cyclicity of their restricted representations.

  1. lemma OAI.WeakPureInfiniteness.finite_quadratic_coefficient_approximation line 19
  2. lemma OAI.WeakPureInfiniteness.unitized_coefficient_representation line 40