OAI/Analysis/BoundedHochschild/MinimalFactors.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Matrix systems in finite factors with minimal projections.

  1. lemma OAI.HochschildMinimalFactor.abelian_of_minimal line 29
  2. lemma OAI.HochschildMinimalFactor.copy_into_nonzero line 43
  3. structure OAI.HochschildMinimalFactor.Packing line 57
  4. def OAI.HochschildMinimalFactor.Packing.total line 64
  5. lemma OAI.HochschildMinimalFactor.Packing.total_proj line 66
  6. lemma OAI.HochschildMinimalFactor.Packing.final_le_total line 80
  7. lemma OAI.HochschildMinimalFactor.Packing.total_trace line 84
  8. lemma OAI.HochschildMinimalFactor.Packing.extend line 90
  9. lemma OAI.HochschildMinimalFactor.exists_full_packing line 121
  10. lemma OAI.HochschildMinimalFactor.abelian_final line 158
  11. def OAI.HochschildMinimalFactor.Packing.matrixSystem line 184
  12. lemma OAI.HochschildMinimalFactor.Packing.matrix_abelian_diagonal line 205
  13. theorem OAI.HochschildMinimalFactor.exists_abelian_matrix_system line 213