OAI/Combinatorics/Chromatic/Walls/QuantumTorusRaySeries.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.QuantumTorus.raySeries line 16
  2. lemma OAI.ElementaryPositivity.QuantumTorus.coeff_raySeries line 18
  3. lemma OAI.ElementaryPositivity.QuantumTorus.raySeries_one line 21
  4. lemma OAI.ElementaryPositivity.QuantumTorus.monomial_sum line 30
  5. lemma OAI.ElementaryPositivity.QuantumTorus.raySeries_mul line 34
  6. lemma OAI.ElementaryPositivity.QuantumTorus.raySeries_twist line 47
  7. def OAI.ElementaryPositivity.QuantumTorus.rayUnit line 78
  8. lemma OAI.ElementaryPositivity.QuantumTorus.ray_adjoint line 87
  9. lemma OAI.ElementaryPositivity.QuantumTorus.ray_inverse_adjoint line 95
  10. def OAI.ElementaryPositivity.QuantumTorus.PositiveCoefficients line 114
  11. lemma OAI.ElementaryPositivity.QuantumTorus.positive_scalar_monomial line 117
  12. lemma OAI.ElementaryPositivity.QuantumTorus.positive_monomial_ray line 127
  13. lemma OAI.ElementaryPositivity.QuantumTorus.positive_elementary_adjoint line 139
  14. lemma OAI.ElementaryPositivity.QuantumTorus.complete_constant line 156
  15. lemma OAI.ElementaryPositivity.QuantumTorus.complete_inverse line 159
  16. lemma OAI.ElementaryPositivity.QuantumTorus.positive_complete_adjoint line 163