OAI/Probability/SignedSweeps/InducedCarrier.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SignedSweeps.fiberSubgroup_sum_factor line 11
  2. def OAI.SignedSweeps.blockEquiv line 32
  3. lemma OAI.SignedSweeps.blockEmbedding_eq line 37
  4. def OAI.SignedSweeps.blockColoring line 41
  5. lemma OAI.SignedSweeps.blockColoring_factor line 45
  6. def OAI.SignedSweeps.Partition.rowIndex line 74
  7. lemma OAI.SignedSweeps.Partition.colOf_lt line 77
  8. def OAI.SignedSweeps.Partition.colIndex line 80
  9. lemma OAI.SignedSweeps.fiberSubgroup_rowIndex line 92
  10. lemma OAI.SignedSweeps.fiberSubgroup_colIndex line 101
  11. def OAI.SignedSweeps.spechtRowVector line 110
  12. lemma OAI.SignedSweeps.spechtRowVector_invariant line 113
  13. lemma OAI.SignedSweeps.spechtRowVector_at_one line 117
  14. lemma OAI.SignedSweeps.spechtRowVector_ne_zero line 135
  15. lemma OAI.SignedSweeps.complex_tmul_ne_zero line 141
  16. lemma OAI.SignedSweeps.signedOccurrence_colorCarrier line 151