OAI/Combinatorics/Chromatic/QuantumTorus/RationalTorusEmbedding.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RationalFiber.embeddedMonomial line 15
2. def OAI.ElementaryPositivity.RationalFiber.embedAdd line 21
3. lemma OAI.ElementaryPositivity.RationalFiber.embedAdd_monomial line 24
4. lemma OAI.ElementaryPositivity.RationalFiber.embeddedMonomial_mul line 30
5. lemma OAI.ElementaryPositivity.RationalFiber.embedAdd_mul line 55
6. lemma OAI.ElementaryPositivity.RationalFiber.embedAdd_one line 65
7. def OAI.ElementaryPositivity.RationalFiber.embed line 68
8. lemma OAI.ElementaryPositivity.RationalFiber.embed_monomial line 72
9. lemma OAI.ElementaryPositivity.RationalFiber.embed_p line 77
10. lemma OAI.ElementaryPositivity.RationalFiber.embed_complement line 80