OAI/Combinatorics/Chromatic/QuantumTorus/PureCutTelescoping.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.QuantumTorus.pureCutGauge line 12
2. lemma OAI.ElementaryPositivity.QuantumTorus.foldr_left_mul line 13
3. lemma OAI.ElementaryPositivity.QuantumTorus.foldr_identity line 19
4. lemma OAI.ElementaryPositivity.QuantumTorus.pureCut_local line 22
5. lemma OAI.ElementaryPositivity.QuantumTorus.pureCut_telescope line 38
6. def OAI.ElementaryPositivity.RationalFiber.fiberReciprocalTerm line 65
7. def OAI.ElementaryPositivity.RationalFiber.fiberReciprocalAdd line 69
8. lemma OAI.ElementaryPositivity.RationalFiber.fiberReciprocalAdd_monomial line 71
9. lemma OAI.ElementaryPositivity.RationalFiber.reciprocal_twist line 75
10. lemma OAI.ElementaryPositivity.RationalFiber.fiberReciprocalAdd_mul line 86
11. def OAI.ElementaryPositivity.RationalFiber.fiberReciprocal line 103
12. lemma OAI.ElementaryPositivity.RationalFiber.fiberReciprocal_oppositeInverse line 111