OAI/Combinatorics/Chromatic/Walls/ChartRefinement.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.chart_root_of_ne line 14
2. lemma OAI.ElementaryPositivity.QuantumTorus.chartZero_supported_kernel line 19
3. def OAI.ElementaryPositivity.QuantumTorus.LexSigns line 33
4. theorem OAI.ElementaryPositivity.QuantumTorus.chart_zero_refinement line 37
5. theorem OAI.ElementaryPositivity.QuantumTorus.chart_negative_refinement line 98