OAI/Combinatorics/Chromatic/GradedAlgebra/RationalPureCoefficients.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RationalFiber.centeredRatio line 14
2. lemma OAI.ElementaryPositivity.RationalFiber.centeredRatio_eq line 18
3. lemma OAI.ElementaryPositivity.RationalFiber.read_pure_monomial_shift line 36
4. lemma OAI.ElementaryPositivity.RationalFiber.old_pure_coeff line 59
5. lemma OAI.ElementaryPositivity.RationalFiber.rational_pure_old_coefficient line 68
6. lemma OAI.ElementaryPositivity.QuantumTorus.mul_X_coeff line 95
7. lemma OAI.ElementaryPositivity.QuantumTorus.X_mul_coeff line 108
8. lemma OAI.ElementaryPositivity.QuantumTorus.central_support_zero line 123