OAI/Analysis/Nuclearity/UnitizedCoefficients.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Finite output coefficients in the unitization. Products with elements of the original algebra stay in that algebra. In particular, coefficients from a unital cyclic representation do not require a unit in the original algebra.

  1. lemma OAI.WeakPureInfiniteness.inr_fintype_sum line 17
  2. def OAI.WeakPureInfiniteness.unitizedRightMul line 21
  3. def OAI.WeakPureInfiniteness.unitizedLeftMul line 23
  4. lemma OAI.WeakPureInfiniteness.inr_unitizedRightMul line 25
  5. lemma OAI.WeakPureInfiniteness.inr_unitizedLeftMul line 29
  6. def OAI.WeakPureInfiniteness.unitizedSandwich line 33
  7. lemma OAI.WeakPureInfiniteness.inr_unitizedSandwich line 36
  8. lemma OAI.WeakPureInfiniteness.unitizedSandwich_sub line 41
  9. lemma OAI.WeakPureInfiniteness.norm_unitizedSandwich_le line 46
  10. def OAI.WeakPureInfiniteness.unitizedCoefficientEnlargement line 53
  11. lemma OAI.WeakPureInfiniteness.inr_unitizedCoefficientEnlargement line 57
  12. lemma OAI.WeakPureInfiniteness.unitizedCoefficientEnlargement_inner line 63