OAI/Combinatorics/Chromatic/Walls/IncomingSystem.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.QuantumTorus.rootDegree_finite line 28
  2. def OAI.ElementaryPositivity.QuantumTorus.incomingCovector line 38
  3. def OAI.ElementaryPositivity.QuantumTorus.incomingMiddle line 43
  4. lemma OAI.ElementaryPositivity.QuantumTorus.incomingMiddle_constant line 48
  5. lemma OAI.ElementaryPositivity.QuantumTorus.incomingMiddle_coeff_congr line 53
  6. def OAI.ElementaryPositivity.QuantumTorus.incomingCoefficient line 58
  7. lemma OAI.ElementaryPositivity.QuantumTorus.incomingCoefficient_apply line 69
  8. lemma OAI.ElementaryPositivity.QuantumTorus.incomingCoefficient_graded line 73
  9. lemma OAI.ElementaryPositivity.QuantumTorus.incomingCoefficient_zero line 78
  10. lemma OAI.ElementaryPositivity.QuantumTorus.incomingCoefficient_congr line 85
  11. lemma OAI.ElementaryPositivity.QuantumTorus.torus_sub_apply line 98
  12. lemma OAI.ElementaryPositivity.QuantumTorus.incomingCoefficient_leading line 103
  13. def OAI.ElementaryPositivity.QuantumTorus.incomingSolutionCoefficients line 133
  14. def OAI.ElementaryPositivity.QuantumTorus.incomingSolution line 139
  15. lemma OAI.ElementaryPositivity.QuantumTorus.incomingSolution_constant line 142
  16. lemma OAI.ElementaryPositivity.QuantumTorus.incomingSolution_graded line 147
  17. def OAI.ElementaryPositivity.QuantumTorus.incomingTruncation line 157
  18. lemma OAI.ElementaryPositivity.QuantumTorus.incomingTruncation_lower line 160
  19. lemma OAI.ElementaryPositivity.QuantumTorus.incomingTruncation_top line 164
  20. lemma OAI.ElementaryPositivity.QuantumTorus.incomingSolution_step line 168
  21. lemma OAI.ElementaryPositivity.QuantumTorus.incomingSolution_prescription_difference line 173
  22. lemma OAI.ElementaryPositivity.QuantumTorus.incomingSolution_prescription line 188
  23. theorem OAI.ElementaryPositivity.QuantumTorus.existsUnique_incoming line 198