OAI/Combinatorics/Chromatic/Walls/LineOldTransport.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RationalFiber.oldCoefficientsEqual line 23
2. lemma OAI.ElementaryPositivity.RationalFiber.oldCoefficientsEqual_equivalence line 26
3. lemma OAI.ElementaryPositivity.RationalFiber.oldCoefficientsEqual_mul line 31
4. def OAI.ElementaryPositivity.RationalFiber.lineNegativeUnit line 39
5. lemma OAI.ElementaryPositivity.RationalFiber.actualLine_old_step line 43
6. lemma OAI.ElementaryPositivity.RationalFiber.actualLine_old_cell line 81
7. theorem OAI.ElementaryPositivity.RationalFiber.actualLine_old_transport line 93
8. structure OAI.ElementaryPositivity.QuantumTorus.GenericLineSegment line 127
9. def OAI.ElementaryPositivity.QuantumTorus.GenericLineSegment.start line 137
10. def OAI.ElementaryPositivity.QuantumTorus.GenericLineSegment.finish line 140
11. inductive OAI.ElementaryPositivity.QuantumTorus.GenericLinePath line 143