OAI/Combinatorics/Chromatic/Walls/WallUnitNegative.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.WallUnits.PositiveRay.positive_rescale line 12
2. lemma OAI.ElementaryPositivity.WallUnits.RationalRay.reverse_ratio line 22
3. lemma OAI.ElementaryPositivity.WallUnits.RationalRay.elementary_inverse_ratio_positive line 27
4. lemma OAI.ElementaryPositivity.WallUnits.RationalRay.complete_inverse_ratio_positive line 31
5. lemma OAI.ElementaryPositivity.QuantumTorus.positive_elementary_inverse_adjoint line 47
6. lemma OAI.ElementaryPositivity.QuantumTorus.positive_complete_inverse_adjoint line 64
7. lemma OAI.ElementaryPositivity.QuantumTorus.ray_constant_one line 81
8. lemma OAI.ElementaryPositivity.QuantumTorus.ray_adjoint_no_jump line 88
9. lemma OAI.ElementaryPositivity.QuantumTorus.ray_inverse_adjoint_no_jump line 96
10. lemma OAI.ElementaryPositivity.QuantumTorus.coeff_linear line 117
11. lemma OAI.ElementaryPositivity.QuantumTorus.ray_linear line 121
12. lemma OAI.ElementaryPositivity.QuantumTorus.normalized_constant line 138
13. lemma OAI.ElementaryPositivity.QuantumTorus.normalized_ratio_one line 141
14. lemma OAI.ElementaryPositivity.QuantumTorus.simple_jump line 150