OAI/Combinatorics/Chromatic/Walls/FinitePureMutation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RationalFiber.constantCoeff_inner_const_inv line 11
2. lemma OAI.ElementaryPositivity.RationalFiber.expandFiberInfinity_lattice line 26
3. lemma OAI.ElementaryPositivity.RationalFiber.pureLaurentUnit_actual_val line 36
4. lemma OAI.ElementaryPositivity.RationalFiber.pureLaurentUnit_actual_inv line 42
5. lemma OAI.ElementaryPositivity.RationalFiber.inner_pure_hahn line 48
6. lemma OAI.ElementaryPositivity.RationalFiber.expand_opposite_inverse_actual line 54
7. lemma OAI.ElementaryPositivity.RationalFiber.finite_cut_hahn line 71
8. lemma OAI.ElementaryPositivity.RationalFiber.finite_cut_actual line 95