OAI/Analysis/ModularTheory/NormalWeightTotality.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Normal-ordered finite-weight vectors are total. The scalar inverse cutoffs remove the weight, then the original cyclic vector removes the gauge.

  1. lemma OAI.WeakPureInfiniteness.modularScalar_annihilator_eq_zero line 17
  2. lemma OAI.WeakPureInfiniteness.modularNormalWeight_annihilator_scalar line 69
  3. lemma OAI.WeakPureInfiniteness.modularNormalWeight_annihilator_eq_zero line 117