OAI/Combinatorics/Chromatic/Walls/CompletedPureComparison.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RationalFiber.completedPureUnit line 18
  2. lemma OAI.ElementaryPositivity.RationalFiber.completed_expand_pure line 20
  3. lemma OAI.ElementaryPositivity.RationalFiber.innerHom_one line 36
  4. lemma OAI.ElementaryPositivity.RationalFiber.innerHom_mul line 38
  5. lemma OAI.ElementaryPositivity.RationalFiber.innerHom_inv_cancel line 41
  6. lemma OAI.ElementaryPositivity.RationalFiber.innerHom_cancel_inv line 44
  7. lemma OAI.ElementaryPositivity.RationalFiber.completed_expand_pure_inverse line 47
  8. def OAI.ElementaryPositivity.RationalFiber.oldUnitExpand line 75
  9. def OAI.ElementaryPositivity.RationalFiber.boundedRationalUnit line 79
  10. lemma OAI.ElementaryPositivity.RationalFiber.boundedUnit_expansion line 94
  11. def OAI.ElementaryPositivity.RationalFiber.oldPureUnit line 104
  12. lemma OAI.ElementaryPositivity.RationalFiber.oldPureUnit_expansion line 109
  13. lemma OAI.ElementaryPositivity.RationalFiber.map_innerHom line 113
  14. lemma OAI.ElementaryPositivity.RationalFiber.bounded_conjugation_expansion line 116
  15. inductive OAI.ElementaryPositivity.RationalFiber.ComparisonCrossing line 141
  16. def OAI.ElementaryPositivity.RationalFiber.comparisonOld line 147
  17. def OAI.ElementaryPositivity.RationalFiber.comparisonAction line 152
  18. lemma OAI.ElementaryPositivity.RationalFiber.comparison_expansion line 159
  19. def OAI.ElementaryPositivity.RationalFiber.comparisonWordOld line 180
  20. def OAI.ElementaryPositivity.RationalFiber.comparisonWordAction line 183
  21. lemma OAI.ElementaryPositivity.RationalFiber.comparisonWord_expansion line 186
  22. lemma OAI.ElementaryPositivity.RationalFiber.comparisonWord_loop line 202