OAI/MathematicalPhysics/Heisenberg/PermutationSymbols.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Heisenberg.Pin.permutationSymbol line 15
  2. lemma OAI.Heisenberg.Pin.stable_permutationSymbol line 19
  3. lemma OAI.Heisenberg.Pin.multiAffine_permutationSymbol line 28
  4. lemma OAI.Heisenberg.Pin.permutationSymbol_eval_one line 41
  5. lemma OAI.Heisenberg.Pin.Stable.rename line 45
  6. lemma OAI.Heisenberg.Pin.rename_permutationSymbol line 52
  7. lemma OAI.Heisenberg.Pin.stable_rename_outputs line 60
  8. def OAI.Heisenberg.Pin.lawSymbol line 70
  9. lemma OAI.Heisenberg.Pin.multiAffine_lawSymbol line 73
  10. lemma OAI.Heisenberg.Pin.lawSymbol_eval_one line 82
  11. lemma OAI.Heisenberg.Pin.lawSymbol_ne_zero line 89
  12. lemma OAI.Heisenberg.Pin.swap_output_map line 97
  13. lemma OAI.Heisenberg.Pin.lawSymbol_bernoulli line 106
  14. theorem OAI.Heisenberg.Pin.stable_lawSymbol_bernoulli line 128
  15. lemma OAI.Heisenberg.Pin.lawSymbol_deterministic_output line 136
  16. theorem OAI.Heisenberg.Pin.stable_lawSymbol_limit line 143
  17. def OAI.Heisenberg.Pin.partialSymbol line 164
  18. lemma OAI.Heisenberg.Pin.partialSymbol_insert line 168
  19. lemma OAI.Heisenberg.Pin.pderiv_partialSymbol line 174
  20. def OAI.Heisenberg.Pin.partialLawSymbol line 192
  21. lemma OAI.Heisenberg.Pin.partialLawSymbol_eval_one line 196
  22. lemma OAI.Heisenberg.Pin.partialLawSymbol_ne_zero line 205
  23. lemma OAI.Heisenberg.Pin.pderiv_partialLawSymbol line 213
  24. theorem OAI.Heisenberg.Pin.stable_partialLawSymbol line 220
  25. def OAI.Heisenberg.Pin.outputSymbol line 234
  26. lemma OAI.Heisenberg.Pin.output_extraction line 238
  27. lemma OAI.Heisenberg.Pin.outputSymbol_eval_one line 244
  28. theorem OAI.Heisenberg.Pin.stable_outputSymbol line 248