OAI/Analysis/Nuclearity/RepresentedIdealGeneration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The Tomiyama factor-image argument followed by pure-state excision. The hypothesis is nuclearity of represented quotients of the left factor (Choi–Effros, Duke Math. J. 43 (1976), Corollary 3.3).

  1. theorem OAI.WeakPureInfiniteness.elementary_generation_of_represented_nuclearity line 19