OAI/Combinatorics/Chromatic/Walls/FiniteElementaryAdjoint.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.WallUnits.DegreeBound line 12
2. lemma OAI.ElementaryPositivity.WallUnits.degreeBound_one line 13
3. lemma OAI.ElementaryPositivity.WallUnits.degreeBound_linear line 16
4. lemma OAI.ElementaryPositivity.WallUnits.DegreeBound.mul line 19
5. lemma OAI.ElementaryPositivity.WallUnits.degreeBound_product_linear line 29
6. lemma OAI.ElementaryPositivity.WallUnits.DegreeBound.rescale line 36
7. lemma OAI.ElementaryPositivity.WallUnits.elementary_ratio_degree line 43
8. lemma OAI.ElementaryPositivity.WallUnits.elementary_inverse_ratio_degree line 48
9. lemma OAI.ElementaryPositivity.QuantumTorus.monomial_ray_support line 64
10. lemma OAI.ElementaryPositivity.QuantumTorus.elementary_adjoint_support line 75
11. lemma OAI.ElementaryPositivity.QuantumTorus.elementary_inverse_adjoint_support line 84
12. lemma OAI.ElementaryPositivity.PowerSeriesAdjoint.inverse_inverse line 102
13. lemma OAI.ElementaryPositivity.PowerSeriesAdjoint.adjoint_one line 109
14. lemma OAI.ElementaryPositivity.PowerSeriesAdjoint.adjoint_inverse line 114
15. lemma OAI.ElementaryPositivity.PowerSeriesAdjoint.adjoint_inverse_cancel line 116
16. lemma OAI.ElementaryPositivity.PowerSeriesAdjoint.adjoint_inverse_coeff line 119