OAI/Combinatorics/Chromatic/QuantumTorus/InfinityExpansionFaithful.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.ElementaryPositivity.RationalFiber.expandFiberInfinity_monomial_coeffline 19 - lemma
OAI.ElementaryPositivity.RationalFiber.expandFiberInfinity_read_monomialline 27 - lemma
OAI.ElementaryPositivity.RationalFiber.expandFiberInfinity_readline 48 - lemma
OAI.ElementaryPositivity.RationalFiber.readFiberInfinity_extline 55 - lemma
OAI.ElementaryPositivity.RationalFiber.expandFiberInfinity_injectiveline 73 - lemma
OAI.ElementaryPositivity.RationalFiber.completed_expandFiberInfinity_injectiveline 79