OAI/Analysis/KadisonKastler/PublishedInfiniteType.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Infinite identities in factors

Blackadar, Operator Algebras, III.1.3.4--5 (pp.242--243), proves that an infinite projection has a nonzero properly infinite central part. In a factor the central part is the identity. Only the resulting pair of orthogonal isometries is retained here.

  1. def OAI.KadisonKastler.PublishedInfiniteFactorProperlyInfinite line 17