OAI/MathematicalPhysics/Heisenberg/ExchangeDeterminants.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Heisenberg.Exposure.det_block_extraction line 20
  2. theorem OAI.Heisenberg.Exposure.DeterminantLaw.inl line 31
  3. theorem OAI.Heisenberg.Exposure.DeterminantLaw.reindex line 44
  4. theorem OAI.Heisenberg.Exposure.DeterminantLaw.subtype line 66
  5. lemma OAI.Heisenberg.Exposure.DeterminantLaw.reparam line 76
  6. lemma OAI.Heisenberg.Exposure.DeterminantLaw.const_left line 84
  7. lemma OAI.Heisenberg.Exposure.determinantLaw_constant line 90
  8. def OAI.Heisenberg.Exposure.splitArray line 96
  9. def OAI.Heisenberg.Exposure.orderedProduct line 103
  10. theorem OAI.Heisenberg.Exposure.determinantLaw_array line 107
  11. def OAI.Heisenberg.LayeredExchange.fibers line 127
  12. lemma OAI.Heisenberg.LayeredExchange.fibers_apply line 133
  13. lemma OAI.Heisenberg.LayeredExchange.fibers_one line 136
  14. lemma OAI.Heisenberg.LayeredExchange.fibers_mul line 139
  15. def OAI.Heisenberg.LayeredExchange.wiring line 142
  16. lemma OAI.Heisenberg.LayeredExchange.wiring_apply line 145
  17. lemma OAI.Heisenberg.LayeredExchange.fibers_update line 148
  18. lemma OAI.Heisenberg.LayeredExchange.fibers_swap line 153
  19. lemma OAI.Heisenberg.Exposure.orderedProduct_map line 170
  20. lemma OAI.Heisenberg.Exposure.orderedProduct_one line 176
  21. lemma OAI.Heisenberg.Exposure.orderedProduct_single line 182
  22. def OAI.Heisenberg.LayeredExchange.fibersHom line 201
  23. lemma OAI.Heisenberg.LayeredExchange.fibers_ordered_product line 206
  24. def OAI.Heisenberg.LayeredExchange.forwardHom line 228
  25. lemma OAI.Heisenberg.LayeredExchange.forwardHom_swap line 233
  26. lemma OAI.Heisenberg.LayeredExchange.determinantLaw_phase line 237
  27. theorem OAI.Heisenberg.LayeredExchange.determinantLaw_wiring line 259