OAI/Combinatorics/Chromatic/Walls/PolynomialIncomingPerturbation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.rootSectionChart_action line 17
2. def OAI.ElementaryPositivity.QuantumTorus.polynomialSectionOrderBound line 23
3. def OAI.ElementaryPositivity.QuantumTorus.polynomialSectionIncoming line 26
4. lemma OAI.ElementaryPositivity.QuantumTorus.monomialSection_incoming_perturbation line 30
5. lemma OAI.ElementaryPositivity.QuantumTorus.actualPolynomialAdjointCoefficient_congr line 53
6. lemma OAI.ElementaryPositivity.QuantumTorus.polynomialSection_incoming_perturbation line 63