OAI/Combinatorics/Chromatic/GradedAlgebra/MutatedPureFace.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.ElementaryPositivity.QuantumTorus.pureFaceSeries_of_pureline 17 - lemma
OAI.ElementaryPositivity.QuantumTorus.pureFaceSeries_kernel_oneline 29 - lemma
OAI.ElementaryPositivity.QuantumTorus.pureFaceSeries_orient_simpleline 55 - lemma
OAI.ElementaryPositivity.QuantumTorus.mutatedLineFactor_pureline 78