OAI/Combinatorics/Chromatic/Walls/MutationInfinityAlgebra.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.ElementaryPositivity.QuantumTorus.infinityCompletedUnit_mulline 21 - lemma
OAI.ElementaryPositivity.QuantumTorus.infinityCompletedUnit_oneline 34 - lemma
OAI.ElementaryPositivity.QuantumTorus.infinityCompletedUnit_inverseline 41 - lemma
OAI.ElementaryPositivity.QuantumTorus.mutatedLaurent_coeff_congrline 51 - lemma
OAI.ElementaryPositivity.QuantumTorus.infinityCompletedUnit_pureline 60 - lemma
OAI.ElementaryPositivity.RationalFiber.completed_expand_oppositeline 99 - lemma
OAI.ElementaryPositivity.RationalFiber.mutation_infinity_oriented_coefficientline 121