OAI/Analysis/Nuclearity/CommutingCutZero.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Cutting both factors of a small positive commuting product gives zero. This is the exact spectral step used to turn tensor excision estimates into elementary tensors in a closed ideal.

  1. theorem OAI.WeakPureInfiniteness.commutative_positive_cut_product_zero line 15
  2. theorem OAI.WeakPureInfiniteness.commutative_mainGap_cut_product_zero line 51
  3. theorem OAI.WeakPureInfiniteness.positive_commuting_cut_product_zero line 60