OAI/Analysis/BoundedHochschild/FiniteGroupBarOperators.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BoundedHochschild.KadisonRingrose.curryMid_one_norm_le line 12
  2. def OAI.BoundedHochschild.KadisonRingrose.barInsertion line 23
  3. lemma OAI.BoundedHochschild.KadisonRingrose.barInsertion_apply line 27
  4. lemma OAI.BoundedHochschild.KadisonRingrose.barInsertion_value line 31
  5. lemma OAI.BoundedHochschild.KadisonRingrose.barInsertion_norm line 43
  6. lemma OAI.BoundedHochschild.KadisonRingrose.barInsertion_add line 47
  7. lemma OAI.BoundedHochschild.KadisonRingrose.barInsertion_smul line 52
  8. def OAI.BoundedHochschild.KadisonRingrose.finiteGroupBarInsertion line 59
  9. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupBarInsertion_norm line 64
  10. def OAI.BoundedHochschild.KadisonRingrose.finiteGroupBarOperator line 78
  11. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupBarOperator_norm line 81
  12. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupBarInsertion_add line 93
  13. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupBarInsertion_smul line 98
  14. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupBarOperator_add line 104
  15. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupBarOperator_smul line 108
  16. def OAI.BoundedHochschild.KadisonRingrose.finiteGroupBarOperatorCLM line 115