OAI/Combinatorics/Chromatic/Walls/FiniteWallCrossing.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.inverse_adjoint_coeff_congr line 14
2. lemma OAI.ElementaryPositivity.QuantumTorus.cut_adjoint_coeff line 23
3. lemma OAI.ElementaryPositivity.QuantumTorus.cut_inverse_adjoint_coeff line 27
4. lemma OAI.ElementaryPositivity.QuantumTorus.rootClosed_isotropic_adjoint line 30
5. lemma OAI.ElementaryPositivity.QuantumTorus.rootClosed_ray_adjoint line 61
6. lemma OAI.ElementaryPositivity.QuantumTorus.ray_charge_through line 101
7. lemma OAI.ElementaryPositivity.QuantumTorus.ray_increment_positive line 114
8. lemma OAI.ElementaryPositivity.QuantumTorus.monomialJump_ray_positive line 145