OAI/MathematicalPhysics/Heisenberg/StablePinLaw.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Heisenberg.Transport.pow_congr line 31
  2. lemma OAI.Heisenberg.Transport.sameCycle_congr line 37
  3. def OAI.Heisenberg.Transport.classCongr line 52
  4. lemma OAI.Heisenberg.Transport.classCongr_mk line 55
  5. lemma OAI.Heisenberg.Transport.missing_pred_congr line 58
  6. lemma OAI.Heisenberg.Transport.missingCount_congr line 72
  7. lemma OAI.Heisenberg.Transport.firstValue_congr_at_hit line 77
  8. lemma OAI.Heisenberg.Transport.nextPoint_congr line 88
  9. lemma OAI.Heisenberg.Transport.nextPermutation_congr line 99
  10. def OAI.Heisenberg.Transport.somePins line 108
  11. lemma OAI.Heisenberg.Transport.somePins_apply line 114
  12. lemma OAI.Heisenberg.Transport.nextPoint_splice line 117
  13. lemma OAI.Heisenberg.Transport.nextPermutation_splice line 126
  14. lemma OAI.Heisenberg.Transport.missingCount_univ line 135
  15. lemma OAI.Heisenberg.Transport.nextPoint_all line 141
  16. lemma OAI.Heisenberg.Transport.nextPermutation_all line 147
  17. lemma OAI.Heisenberg.Pin.permutationSymbol_congr line 164
  18. lemma OAI.Heisenberg.Pin.lawSymbol_congr line 173
  19. lemma OAI.Heisenberg.Pin.stable_law_congr line 178
  20. def OAI.Heisenberg.Pin.pinLaw line 183
  21. lemma OAI.Heisenberg.Pin.pinLaw_all line 187
  22. lemma OAI.Heisenberg.Pin.stable_pinLaw_all line 197
  23. lemma OAI.Heisenberg.Pin.splice_mass_nonneg line 203
  24. lemma OAI.Heisenberg.Pin.splice_mass_pos line 208
  25. theorem OAI.Heisenberg.Pin.stable_pinLaw line 218