OAI/Combinatorics/Chromatic/Walls/MutationSimpleIncoming.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.regrade_homogeneous_identity line 16
2. lemma OAI.ElementaryPositivity.QuantumTorus.normalizedSimple_homogeneous line 40
3. lemma OAI.ElementaryPositivity.QuantumTorus.mutation_incoming_simple_image line 54
4. lemma OAI.ElementaryPositivity.QuantumTorus.mutation_incoming_simple_order line 67
5. lemma OAI.ElementaryPositivity.QuantumTorus.mutation_push_normalizedSimple line 74
6. theorem OAI.ElementaryPositivity.QuantumTorus.mutation_normalized_incoming_simple line 84
7. lemma OAI.ElementaryPositivity.QuantumTorus.mutation_side_simple_image line 103
8. lemma OAI.ElementaryPositivity.QuantumTorus.mutation_side_simple_order line 118
9. lemma OAI.ElementaryPositivity.QuantumTorus.mutation_normalized_simple_side line 126
10. lemma OAI.ElementaryPositivity.QuantumTorus.mutationCompletion_congr_through line 138
11. lemma OAI.ElementaryPositivity.QuantumTorus.actual_simple_wall_mutation_through line 149
12. lemma OAI.ElementaryPositivity.QuantumTorus.actual_simple_wall_mutation line 161