OAI/Combinatorics/Chromatic/Walls/InfinityPath.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RationalFiber.mutatedPathProduct_constant line 23
2. lemma OAI.ElementaryPositivity.RationalFiber.mutatedPathProduct_graded line 31
3. def OAI.ElementaryPositivity.RationalFiber.mutatedPathProductPositive line 40
4. def OAI.ElementaryPositivity.RationalFiber.actualInfinityPathProductUnit line 46
5. lemma OAI.ElementaryPositivity.RationalFiber.actualInfinityPathProductUnit_nil line 51
6. lemma OAI.ElementaryPositivity.RationalFiber.actualInfinityPathProductUnit_append line 55
7. lemma OAI.ElementaryPositivity.RationalFiber.actualInfinityPath_product_square line 64
8. lemma OAI.ElementaryPositivity.RationalFiber.infinitySideHom_coeff_congr line 98
9. lemma OAI.ElementaryPositivity.RationalFiber.infinity_embed_X line 112
10. def OAI.ElementaryPositivity.RationalFiber.infinityTestInput line 128
11. lemma OAI.ElementaryPositivity.RationalFiber.infinitySideHom_test line 133