OAI/Combinatorics/Chromatic/Walls/IncomingEquality.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.QuantumTorus.literalTotalTransport_log_ray line 12
  2. lemma OAI.ElementaryPositivity.QuantumTorus.literal_incoming_at_far_through line 38
  3. def OAI.ElementaryPositivity.QuantumTorus.shearCovector line 80
  4. def OAI.ElementaryPositivity.QuantumTorus.shearCovectorInverse line 81
  5. lemma OAI.ElementaryPositivity.QuantumTorus.shearCovector_at_p line 83
  6. lemma OAI.ElementaryPositivity.QuantumTorus.shearCovectorInverse_at_p line 87
  7. lemma OAI.ElementaryPositivity.QuantumTorus.shearCovector_inv line 91
  8. lemma OAI.ElementaryPositivity.QuantumTorus.shearCovector_inv' line 96
  9. lemma OAI.ElementaryPositivity.QuantumTorus.shearCovector_on_cut line 100
  10. def OAI.ElementaryPositivity.QuantumTorus.mutationCovector line 105
  11. def OAI.ElementaryPositivity.QuantumTorus.mutationCovectorInverse line 107
  12. lemma OAI.ElementaryPositivity.QuantumTorus.mutationCovector_at_p line 110
  13. lemma OAI.ElementaryPositivity.QuantumTorus.mutationCovectorInverse_at_p line 114
  14. lemma OAI.ElementaryPositivity.QuantumTorus.mutationCovector_left_inverse line 118
  15. lemma OAI.ElementaryPositivity.QuantumTorus.mutationCovector_right_inverse line 125
  16. def OAI.ElementaryPositivity.QuantumTorus.mutationCovectorEquiv line 132
  17. lemma OAI.ElementaryPositivity.QuantumTorus.incoming_shear_covariance line 138
  18. def OAI.ElementaryPositivity.QuantumTorus.mutationIncomingLabel line 146
  19. def OAI.ElementaryPositivity.QuantumTorus.mutationIncomingLabelInverse line 147
  20. lemma OAI.ElementaryPositivity.QuantumTorus.mutationIncomingLabel_pairing line 149
  21. lemma OAI.ElementaryPositivity.QuantumTorus.mutationIncomingLabelInverse_pairing line 153
  22. lemma OAI.ElementaryPositivity.QuantumTorus.mutationIncomingLabel_left_inverse line 157
  23. lemma OAI.ElementaryPositivity.QuantumTorus.mutationIncomingLabel_right_inverse line 163
  24. def OAI.ElementaryPositivity.QuantumTorus.mutationIncomingLabelEquiv line 168
  25. lemma OAI.ElementaryPositivity.QuantumTorus.mutationIncomingLabel_nonnegative line 173
  26. lemma OAI.ElementaryPositivity.QuantumTorus.mutationIncomingLabel_nonpositive line 175
  27. lemma OAI.ElementaryPositivity.QuantumTorus.incoming_mutation_covariance line 179