OAI/Combinatorics/Chromatic/Walls/SectionIncoming.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.QuantumTorus.sectionIncoming line 18
  2. lemma OAI.ElementaryPositivity.QuantumTorus.sectionIncoming_apply line 23
  3. lemma OAI.ElementaryPositivity.QuantumTorus.sectionIncoming_graded line 26
  4. lemma OAI.ElementaryPositivity.QuantumTorus.sectionIncoming_congr line 30
  5. lemma OAI.ElementaryPositivity.QuantumTorus.sectionIncoming_leading line 40
  6. lemma OAI.ElementaryPositivity.QuantumTorus.sectionIncoming_zero line 54
  7. def OAI.ElementaryPositivity.QuantumTorus.sectionSolutionCoefficients line 66
  8. def OAI.ElementaryPositivity.QuantumTorus.sectionSolution line 72
  9. def OAI.ElementaryPositivity.QuantumTorus.sectionTruncation line 74
  10. lemma OAI.ElementaryPositivity.QuantumTorus.sectionSolution_graded line 76
  11. lemma OAI.ElementaryPositivity.QuantumTorus.sectionTruncation_lower line 85
  12. lemma OAI.ElementaryPositivity.QuantumTorus.sectionTruncation_top line 88
  13. lemma OAI.ElementaryPositivity.QuantumTorus.sectionSolution_step line 91
  14. lemma OAI.ElementaryPositivity.QuantumTorus.sectionSolution_prescription line 95
  15. theorem OAI.ElementaryPositivity.QuantumTorus.existsUnique_section line 112
  16. def OAI.ElementaryPositivity.QuantumTorus.thetaInitial line 129
  17. def OAI.ElementaryPositivity.QuantumTorus.thetaValue line 131
  18. lemma OAI.ElementaryPositivity.QuantumTorus.thetaInitial_graded line 133
  19. lemma OAI.ElementaryPositivity.QuantumTorus.thetaValue_graded line 135
  20. lemma OAI.ElementaryPositivity.QuantumTorus.thetaInitial_prescription line 137
  21. lemma OAI.ElementaryPositivity.QuantumTorus.thetaValue_leading line 141