OAI/Combinatorics/Chromatic/Walls/WallRegrade.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.QuantumTorus.rootOrder line 14
  2. lemma OAI.ElementaryPositivity.QuantumTorus.rootOrder_eq line 20
  3. lemma OAI.ElementaryPositivity.QuantumTorus.chart_full_homogeneous line 28
  4. lemma OAI.ElementaryPositivity.QuantumTorus.simple_regrade_bound line 39
  5. lemma OAI.ElementaryPositivity.QuantumTorus.simple_inverse_regrade_bound line 56
  6. def OAI.ElementaryPositivity.QuantumTorus.mutationPieceEquiv line 77
  7. lemma OAI.ElementaryPositivity.QuantumTorus.mutationPieceEquiv_apply line 79
  8. lemma OAI.ElementaryPositivity.QuantumTorus.mutationLinearPiece_pairing line 83
  9. lemma OAI.ElementaryPositivity.QuantumTorus.mutationLinearPiece_injective line 89
  10. lemma OAI.ElementaryPositivity.QuantumTorus.mutationLinearPiece_surjective line 94
  11. def OAI.ElementaryPositivity.QuantumTorus.mutationNewOrder line 101
  12. lemma OAI.ElementaryPositivity.QuantumTorus.mutationNewOrder_of_root line 105
  13. def OAI.ElementaryPositivity.QuantumTorus.mutationTorusPush line 116
  14. lemma OAI.ElementaryPositivity.QuantumTorus.mutationTorusPush_read line 119
  15. def OAI.ElementaryPositivity.QuantumTorus.mutationCompletion line 123
  16. lemma OAI.ElementaryPositivity.QuantumTorus.mutationCompletion_coeff_read line 127
  17. lemma OAI.ElementaryPositivity.QuantumTorus.mutationCompletion_bound line 134
  18. lemma OAI.ElementaryPositivity.QuantumTorus.mutationCompletion_graded line 144
  19. lemma OAI.ElementaryPositivity.QuantumTorus.mutationCompletion_constant line 162
  20. def OAI.ElementaryPositivity.QuantumTorus.mutationCompletedPositive line 169
  21. lemma OAI.ElementaryPositivity.QuantumTorus.mutationCompletion_mul line 176
  22. lemma OAI.ElementaryPositivity.QuantumTorus.mutationCompletion_one line 183
  23. lemma OAI.ElementaryPositivity.QuantumTorus.mutationCompletion_inverse_mul line 185
  24. lemma OAI.ElementaryPositivity.QuantumTorus.mutationCompletion_mul_inverse line 192
  25. def OAI.ElementaryPositivity.QuantumTorus.actualMutatedWall line 206