OAI/Probability/SignedSweeps/WordGrouping.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.groupWordEquiv line 12
  2. def OAI.SignedSweeps.groupedWordMatrix line 25
  3. lemma OAI.SignedSweeps.groupedWordMatrix_mul line 30
  4. lemma OAI.SignedSweeps.groupedWordMatrix_one line 38
  5. lemma OAI.SignedSweeps.groupedWordMatrix_star line 44
  6. lemma OAI.SignedSweeps.groupedWordMatrix_positive line 50
  7. lemma OAI.SignedSweeps.groupedWordMatrix_lower line 55
  8. lemma OAI.SignedSweeps.groupedWordMatrix_scale line 63
  9. lemma OAI.SignedSweeps.groupedWordMatrix_trace line 70
  10. lemma OAI.SignedSweeps.groupedWordMatrix_tensor line 78
  11. lemma OAI.SignedSweeps.groupedWordMatrix_const_tensor line 93
  12. lemma OAI.SignedSweeps.groupedWordMatrix_commute line 99
  13. def OAI.SignedSweeps.groupedWordOperator line 106
  14. lemma OAI.SignedSweeps.groupedWordOperator_mul line 111
  15. lemma OAI.SignedSweeps.groupedWordOperator_positive line 116
  16. lemma OAI.SignedSweeps.groupedWordOperator_idempotent line 124
  17. lemma OAI.SignedSweeps.groupedWordMatrix_toEuclideanLin line 130