OAI/Combinatorics/Chromatic/GradedAlgebra/BoundedWordLaurent.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RationalFiber.ComparisonCrossing.IsBounded line 13
2. lemma OAI.ElementaryPositivity.RationalFiber.boundedAction_preserves_laurent line 16
3. lemma OAI.ElementaryPositivity.RationalFiber.boundedWord_preserves_laurent line 28
4. lemma OAI.ElementaryPositivity.RationalFiber.actualLineLetter_bounded line 54
5. lemma OAI.ElementaryPositivity.RationalFiber.actualLineWord_bounded line 67
6. lemma OAI.ElementaryPositivity.RationalFiber.actualPathWord_bounded line 80
7. theorem OAI.ElementaryPositivity.RationalFiber.actualPathAction_finite_laurent line 92