OAI/Analysis/PureInfiniteness/RelativeCornerSums.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite orthogonal corner sums use relative support relations rather than isometries in a unital algebra. These are the finite Cuntz-sum identities needed for combining abelian-range maps on selected positive tests.

  1. def OAI.WeakPureInfiniteness.relativeCornerSum line 16
  2. lemma OAI.WeakPureInfiniteness.relativeCornerSum_mul line 18
  3. lemma OAI.WeakPureInfiniteness.relativeCornerSum_commute line 35
  4. lemma OAI.WeakPureInfiniteness.relativeCornerSum_coefficient line 48
  5. lemma OAI.WeakPureInfiniteness.relativeCornerSum_compression line 73