OAI/Combinatorics/Chromatic/Walls/PlanarRefinement.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.real_incoming_covector line 18
2. lemma OAI.ElementaryPositivity.QuantumTorus.real_perturbed_covector line 23
3. lemma OAI.ElementaryPositivity.QuantumTorus.linear_zero_on_plane line 29
4. lemma OAI.ElementaryPositivity.QuantumTorus.planar_refinement_generic line 35
5. lemma OAI.ElementaryPositivity.QuantumTorus.joint_roots_plane line 70
6. lemma OAI.ElementaryPositivity.QuantumTorus.joint_cut_supported line 79
7. def OAI.ElementaryPositivity.QuantumTorus.WallsPositiveThrough line 105
8. lemma OAI.ElementaryPositivity.QuantumTorus.line_plus_covector line 115
9. lemma OAI.ElementaryPositivity.QuantumTorus.line_minus_covector line 122
10. theorem OAI.ElementaryPositivity.QuantumTorus.wall_joint_induction line 129