OAI/Combinatorics/Chromatic/QuantumTorus/NormalizedMonomialAction.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ElementaryPositivity.QuantumTorus.normalizedMonomialActionline 16 - lemma
OAI.ElementaryPositivity.QuantumTorus.adjoint_monomial_normalizedline 20 - lemma
OAI.ElementaryPositivity.QuantumTorus.normalizedMonomialAction_boundline 31 - lemma
OAI.ElementaryPositivity.QuantumTorus.normalizedMonomialAction_constantline 36 - lemma
OAI.ElementaryPositivity.QuantumTorus.adjoint_monomial_coeffline 43 - lemma
OAI.ElementaryPositivity.QuantumTorus.normalizedMonomialAction_gradedline 55