OAI/Combinatorics/Chromatic/GradedAlgebra/LaurentRegradeFinite.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.sum_range_eq_of_tails_zero line 17
2. lemma OAI.ElementaryPositivity.QuantumTorus.laurentRegrade_off_diagonal line 27
3. lemma OAI.ElementaryPositivity.QuantumTorus.laurentRegrade_finite line 36
4. lemma OAI.ElementaryPositivity.QuantumTorus.laurentRegrade_finite_read line 64