OAI/Combinatorics/Chromatic/Walls/MutatedLineCompletion.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.PowerSeriesAdjoint.filter_product_coeff_congr line 11
2. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedLineProduct_stabilizes line 48
3. def OAI.ElementaryPositivity.QuantumTorus.mutatedLineCompletion line 60
4. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedLineCompletion_coeff line 64
5. lemma OAI.ElementaryPositivity.QuantumTorus.orientPowerSeries_constant line 81
6. lemma OAI.ElementaryPositivity.QuantumTorus.orientPowerSeries_graded line 96
7. lemma OAI.ElementaryPositivity.QuantumTorus.mutationCompletion_inverse line 103
8. lemma OAI.ElementaryPositivity.QuantumTorus.mutationCompletion_orient_graded line 120
9. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedLineFactor_constant line 140
10. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedLineFactor_graded line 152
11. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedLineProduct_constant line 171
12. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedLineProduct_graded line 180
13. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedLineCompletion_constant line 190
14. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedLineCompletion_graded line 196
15. def OAI.ElementaryPositivity.QuantumTorus.mutatedLineCompletedPositive line 204