OAI/Combinatorics/Chromatic/GradedAlgebra/SimpleBinomial.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.QuantumTorus.normalizedSimple line 13
2. lemma OAI.ElementaryPositivity.QuantumTorus.simpleDatum_value line 17
3. lemma OAI.ElementaryPositivity.QuantumTorus.normalizedSimple_constant line 23
4. lemma OAI.ElementaryPositivity.QuantumTorus.normalizedSimple_inverse line 27
5. lemma OAI.ElementaryPositivity.QuantumTorus.laurent_q_nonzero line 38
6. lemma OAI.ElementaryPositivity.QuantumTorus.laurent_shift_positive line 42
7. lemma OAI.ElementaryPositivity.QuantumTorus.laurent_shift_negative line 50
8. lemma OAI.ElementaryPositivity.QuantumTorus.normalizedSimple_adjoint_support line 56
9. lemma OAI.ElementaryPositivity.QuantumTorus.normalizedSimple_inverse_adjoint_support line 63