OAI/Combinatorics/Chromatic/Walls/FiniteRefinementImportAll.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RationalFiber.finite_refinement_import line 21
2. lemma OAI.ElementaryPositivity.RationalFiber.all_finite_refinements_import line 50
3. def OAI.ElementaryPositivity.RationalFiber.actualLineWord line 79
4. lemma OAI.ElementaryPositivity.RationalFiber.actualLineWord_refines line 85
5. lemma OAI.ElementaryPositivity.RationalFiber.actualLineWord_refinements line 100
6. def OAI.ElementaryPositivity.QuantumTorus.orientPowerSeries line 119
7. lemma OAI.ElementaryPositivity.QuantumTorus.orientPowerSeries_trivial line 121
8. def OAI.ElementaryPositivity.QuantumTorus.mutatedLineFactor line 143
9. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedLineFactor_high line 158
10. def OAI.ElementaryPositivity.QuantumTorus.mutatedLineProduct line 177