OAI/Combinatorics/Chromatic/QuantumTorus/GeometricMutation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.QuantumTorus.realShearCovector line 14
  2. def OAI.ElementaryPositivity.QuantumTorus.realShearCovectorInverse line 15
  3. lemma OAI.ElementaryPositivity.QuantumTorus.realShearCovector_at_p line 17
  4. lemma OAI.ElementaryPositivity.QuantumTorus.realShearCovectorInverse_at_p line 21
  5. lemma OAI.ElementaryPositivity.QuantumTorus.realShearCovector_left_inverse line 25
  6. lemma OAI.ElementaryPositivity.QuantumTorus.realShearCovector_right_inverse line 30
  7. def OAI.ElementaryPositivity.QuantumTorus.realMutationCovector line 35
  8. def OAI.ElementaryPositivity.QuantumTorus.realMutationCovectorInverse line 37
  9. lemma OAI.ElementaryPositivity.QuantumTorus.realMutationCovector_at_p line 40
  10. lemma OAI.ElementaryPositivity.QuantumTorus.realMutationCovectorInverse_at_p line 45
  11. lemma OAI.ElementaryPositivity.QuantumTorus.realMutationCovector_left_inverse line 50
  12. lemma OAI.ElementaryPositivity.QuantumTorus.realMutationCovector_right_inverse line 57
  13. def OAI.ElementaryPositivity.QuantumTorus.realMutationCovectorEquiv line 64
  14. lemma OAI.ElementaryPositivity.QuantumTorus.realShearCovector_lattice line 71
  15. lemma OAI.ElementaryPositivity.QuantumTorus.realMutationCovector_lattice line 79
  16. lemma OAI.ElementaryPositivity.QuantumTorus.realMutationCovector_incoming line 88