OAI/Combinatorics/Chromatic/Walls/IsolatedPositivePlane.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ElementaryPositivity.QuantumTorus.isolated_positive_plane line 19
2. lemma OAI.ElementaryPositivity.QuantumTorus.OnPositiveRay.symm line 113
3. lemma OAI.ElementaryPositivity.QuantumTorus.OnPositiveRay.trans line 116
4. lemma OAI.ElementaryPositivity.QuantumTorus.OnPositiveRay.eq_pred line 127
5. lemma OAI.ElementaryPositivity.QuantumTorus.OnPositiveRay.mem_submodule line 132
6. lemma OAI.ElementaryPositivity.QuantumTorus.OnPositiveRay.pair_nonneg line 140
7. lemma OAI.ElementaryPositivity.QuantumTorus.OnPositiveRay.pair_zero line 150
8. lemma OAI.ElementaryPositivity.QuantumTorus.literalRootProducts_allowed_mono line 158