OAI/Analysis/Nuclearity/RepresentedFactorTensor.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Algebraic faithfulness of the two represented image algebras, for the actual irreducible representation in the ideal-separation argument.

  1. def OAI.WeakPureInfiniteness.leftRepresentedMap line 22
  2. def OAI.WeakPureInfiniteness.rightRepresentedMap line 25
  3. theorem OAI.WeakPureInfiniteness.representedFactor_commute line 28
  4. theorem OAI.WeakPureInfiniteness.representedFactor_tensor_injective line 38