OAI/Combinatorics/Chromatic/GradedAlgebra/RationalLaurentScalars.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.RationalFiber.ratFunc_hom_ext_ring line 13
  2. def OAI.ElementaryPositivity.RationalFiber.innerHom line 25
  3. def OAI.ElementaryPositivity.RationalFiber.expandScalar line 38
  4. lemma OAI.ElementaryPositivity.RationalFiber.expandScalar_C line 40
  5. lemma OAI.ElementaryPositivity.RationalFiber.expandScalar_X line 45
  6. lemma OAI.ElementaryPositivity.RationalFiber.torus_X_unit line 52
  7. def OAI.ElementaryPositivity.RationalFiber.constUnit line 54
  8. lemma OAI.ElementaryPositivity.RationalFiber.pairing_swap line 63
  9. lemma OAI.ElementaryPositivity.RationalFiber.constUnit_conj_C line 67
  10. lemma OAI.ElementaryPositivity.RationalFiber.constUnit_conj_X line 74
  11. lemma OAI.ElementaryPositivity.RationalFiber.scalar_commutation line 86
  12. def OAI.ElementaryPositivity.RationalFiber.expandFiberTerm line 128
  13. def OAI.ElementaryPositivity.RationalFiber.expandFiberAdd line 132
  14. lemma OAI.ElementaryPositivity.RationalFiber.expandFiberAdd_monomial line 134
  15. lemma OAI.ElementaryPositivity.RationalFiber.const_torus_product line 138
  16. lemma OAI.ElementaryPositivity.RationalFiber.expandFiberAdd_monomial_mul line 144
  17. lemma OAI.ElementaryPositivity.RationalFiber.expandFiberAdd_mul line 158
  18. lemma OAI.ElementaryPositivity.RationalFiber.expandFiberAdd_one line 169
  19. def OAI.ElementaryPositivity.RationalFiber.expandFiber line 173