OAI/Combinatorics/Chromatic/Walls/FiniteSignCharts.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.chartZero_congr_through line 14
2. lemma OAI.ElementaryPositivity.QuantumTorus.chart_sign_congr_through line 20
3. def OAI.ElementaryPositivity.QuantumTorus.RayGeneric line 37
4. lemma OAI.ElementaryPositivity.QuantumTorus.RayGeneric.mono line 39
5. lemma OAI.ElementaryPositivity.QuantumTorus.RayGeneric.ray_supported line 43
6. lemma OAI.ElementaryPositivity.QuantumTorus.RootClosedThrough.reduce line 59
7. theorem OAI.ElementaryPositivity.QuantumTorus.positive_joint_transport line 88