OAI/Analysis/Nuclearity/UnitizedIdealGeneration.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Transfer of elementary ideal generation from the left unitization to its original nonunital tensor ideal.

  1. theorem OAI.WeakPureInfiniteness.unitizationInr_rightIdeal line 18
  2. theorem OAI.WeakPureInfiniteness.unitizedTensorInclusion_rightIdeal line 26
  3. theorem OAI.WeakPureInfiniteness.elementary_generation_of_unitization line 37