OAI/Combinatorics/Chromatic/Walls/LaurentCompletionFaithful.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.laurentRegrade_central_faithful line 20
2. lemma OAI.ElementaryPositivity.WallUnits.LaurentRay.vUnit_zpow_injective line 62
3. lemma OAI.ElementaryPositivity.QuantumTorus.laurent_completed_adjoint_faithful line 75
4. lemma OAI.ElementaryPositivity.RationalFiber.mutatedPathCompleted_loop_row_commute line 105
5. lemma OAI.ElementaryPositivity.RationalFiber.mutatedPathCompletion_loop line 133