OAI/MathematicalPhysics/Heisenberg/PinSplicing.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Heisenberg.Pin.spliceVariables line 18
  2. def OAI.Heisenberg.Pin.eraseNone line 24
  3. def OAI.Heisenberg.Pin.splice line 27
  4. lemma OAI.Heisenberg.Pin.eraseNone_rename_some line 30
  5. lemma OAI.Heisenberg.Pin.pderiv_none_rename_some line 39
  6. lemma OAI.Heisenberg.Pin.eraseNone_X_none line 47
  7. lemma OAI.Heisenberg.Pin.eraseNone_X_some line 50
  8. lemma OAI.Heisenberg.Pin.renamed_symbol_fixed line 54
  9. theorem OAI.Heisenberg.Pin.splice_permutationSymbol_fixed line 69
  10. lemma OAI.Heisenberg.Pin.removeNone_at_predecessor line 77
  11. lemma OAI.Heisenberg.Pin.removeNone_off_predecessor line 82
  12. lemma OAI.Heisenberg.Pin.renamed_symbol_spliced line 91
  13. theorem OAI.Heisenberg.Pin.splice_permutationSymbol_nonfixed line 110
  14. lemma OAI.Heisenberg.Pin.eraseNone_eq_boundarySection line 129
  15. theorem OAI.Heisenberg.Pin.stable_splice line 138
  16. lemma OAI.Heisenberg.Pin.splice_add line 150
  17. lemma OAI.Heisenberg.Pin.splice_C_mul line 154
  18. lemma OAI.Heisenberg.Pin.splice_sum line 161
  19. def OAI.Heisenberg.Pin.spliceWeight line 164
  20. lemma OAI.Heisenberg.Pin.spliceWeight_ge_one line 167
  21. lemma OAI.Heisenberg.Pin.splice_permutationSymbol line 171
  22. lemma OAI.Heisenberg.Pin.splice_lawSymbol line 180
  23. lemma OAI.Heisenberg.Pin.lawSymbol_eval_one_general line 187
  24. lemma OAI.Heisenberg.Pin.lawSymbol_ne_zero_general line 196
  25. theorem OAI.Heisenberg.Pin.stable_spliced_law line 203
  26. def OAI.Heisenberg.Cycle.projection line 225
  27. lemma OAI.Heisenberg.Cycle.projection_apply line 229
  28. lemma OAI.Heisenberg.Cycle.projection_pow line 247
  29. lemma OAI.Heisenberg.Cycle.sameCycle_removeNone_iff line 256
  30. def OAI.Heisenberg.Cycle.classInclusion line 285
  31. lemma OAI.Heisenberg.Cycle.classInclusion_mk line 288
  32. lemma OAI.Heisenberg.Cycle.classInclusion_injective line 291
  33. lemma OAI.Heisenberg.Cycle.classInclusion_surjective line 299
  34. lemma OAI.Heisenberg.Cycle.classInclusion_range_fixed line 312
  35. lemma OAI.Heisenberg.Cycle.missingInclusion_condition line 326
  36. def OAI.Heisenberg.Cycle.missingInclusion line 337
  37. lemma OAI.Heisenberg.Cycle.missingInclusion_injective line 341
  38. lemma OAI.Heisenberg.Cycle.missingInclusion_surjective line 347
  39. lemma OAI.Heisenberg.Cycle.missingCount_nonfixed line 354
  40. lemma OAI.Heisenberg.Cycle.none_missing line 361
  41. def OAI.Heisenberg.Cycle.missingOption line 367
  42. lemma OAI.Heisenberg.Cycle.missingOption_injective line 372
  43. lemma OAI.Heisenberg.Cycle.missingOption_surjective line 396
  44. lemma OAI.Heisenberg.Cycle.missingCount_fixed line 409
  45. theorem OAI.Heisenberg.Cycle.cycle_weight_splice line 417