OAI/Analysis/Nuclearity/ElementaryGeneratedIdeal.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The closed span of the elementary tensors in a closed tensor ideal is itself an ideal. This does not assert that it is the whole original ideal.

  1. def OAI.WeakPureInfiniteness.elementaryIdealSpan line 16
  2. lemma OAI.WeakPureInfiniteness.elementaryIdealSpan_mul_left line 20
  3. lemma OAI.WeakPureInfiniteness.elementaryIdealSpan_mul_right line 32
  4. lemma OAI.WeakPureInfiniteness.elementaryIdealSpan_star line 44
  5. def OAI.WeakPureInfiniteness.elementaryGeneratedIdeal line 56
  6. theorem OAI.WeakPureInfiniteness.elementaryGeneratedIdeal_le line 102
  7. theorem OAI.WeakPureInfiniteness.elementary_mem_generatedIdeal line 109