OAI/Combinatorics/Chromatic/GradedAlgebra/RootMutationInventory.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.ElementaryPositivity.QuantumTorus.simpleRoot_injectiveline 16 - def
OAI.ElementaryPositivity.QuantumTorus.rootMutationline 25 - lemma
OAI.ElementaryPositivity.QuantumTorus.mutatedRoot_inventoryline 29 - lemma
OAI.ElementaryPositivity.QuantumTorus.mutatedRoot_listline 41 - lemma
OAI.ElementaryPositivity.QuantumTorus.rootMutation_map_offline 47 - lemma
OAI.ElementaryPositivity.QuantumTorus.rootMutation_rotation_permline 54 - lemma
OAI.ElementaryPositivity.QuantumTorus.rootMutation_gaps_fixedline 65