OAI/Combinatorics/Chromatic/QuantumTorus/OrbitMonomialSymmetric.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.OrbitMonomial.exponentOrbit line 12
2. def OAI.ElementaryPositivity.OrbitMonomial.polynomial line 15
3. lemma OAI.ElementaryPositivity.OrbitMonomial.exponentOrbit_self line 18
4. lemma OAI.ElementaryPositivity.OrbitMonomial.exponentOrbit_map line 22
5. lemma OAI.ElementaryPositivity.OrbitMonomial.exponentOrbit_map_iff line 28
6. lemma OAI.ElementaryPositivity.OrbitMonomial.coeff_polynomial line 36
7. lemma OAI.ElementaryPositivity.OrbitMonomial.polynomial_symmetric line 40
8. lemma OAI.ElementaryPositivity.OrbitMonomial.polynomial_homogeneous line 50
9. lemma OAI.ElementaryPositivity.OrbitMonomial.dominant_orbit_unique line 57
10. lemma OAI.ElementaryPositivity.OrbitMonomial.dominant_coeff line 74
11. lemma OAI.ElementaryPositivity.OrbitMonomial.exponentOrbit_symm line 91
12. lemma OAI.ElementaryPositivity.OrbitMonomial.exponentOrbit_trans line 95
13. lemma OAI.ElementaryPositivity.OrbitMonomial.symmetric_coeff_orbit line 99
14. lemma OAI.ElementaryPositivity.OrbitMonomial.dominant_representative line 105
15. lemma OAI.ElementaryPositivity.OrbitMonomial.symmetric_orbit_decomposition line 118