OAI/MathematicalPhysics/Heisenberg/DeterminantExposure.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Heisenberg.Exposure.det_two_rows line 14
  2. def OAI.Heisenberg.Exposure.swapMix line 39
  3. lemma OAI.Heisenberg.Exposure.one_sub_swapMix_mul line 42
  4. theorem OAI.Heisenberg.Exposure.det_swapMix line 71
  5. def OAI.Heisenberg.Exposure.DeterminantLaw line 88
  6. theorem OAI.Heisenberg.Exposure.determinantLaw_bernoulli line 94
  7. lemma OAI.Heisenberg.Exposure.determinantLaw_deterministic line 103
  8. theorem OAI.Heisenberg.Exposure.DeterminantLaw.independent_mul line 108
  9. def OAI.Heisenberg.Exposure.partialMatrix line 151
  10. def OAI.Heisenberg.Exposure.walk line 154
  11. lemma OAI.Heisenberg.Exposure.walk_add line 159
  12. lemma OAI.Heisenberg.Exposure.walk_eq_none_of_le line 170
  13. lemma OAI.Heisenberg.Exposure.pow_partialMatrix line 176
  14. def OAI.Heisenberg.Exposure.Escapes line 189
  15. lemma OAI.Heisenberg.Exposure.escapes_of_none line 192
  16. lemma OAI.Heisenberg.Exposure.escapes_iff_of_some line 196
  17. lemma OAI.Heisenberg.Exposure.nilpotent_partialMatrix line 206
  18. lemma OAI.Heisenberg.Exposure.det_one_sub_of_nilpotent line 217
  19. lemma OAI.Heisenberg.Exposure.det_one_sub_partialMatrix_of_not_all line 225
  20. theorem OAI.Heisenberg.Exposure.det_one_sub_partialMatrix line 246