OAI/Analysis/ModularTheory/CornerProductNorm.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite sums of actual corner products have their finite-tracial GNS norm.

  1. lemma OAI.WeakPureInfiniteness.modularCornerProduct_right_support line 17
  2. lemma OAI.WeakPureInfiniteness.modularCornerProduct_sum_norm line 43