OAI/Combinatorics/Chromatic/Shuffle/FourBraiding.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.crossingColumnBAlg line 34
  2. def OAI.ElementaryPositivity.RawShuffle.fourUnitalFiltration line 38
  3. lemma OAI.ElementaryPositivity.RawShuffle.fourBraidingCoefficient_next line 43
  4. lemma OAI.ElementaryPositivity.RawShuffle.map_sub_one_mul line 57
  5. lemma OAI.ElementaryPositivity.RawShuffle.fourBraiding_coeff_next line 60
  6. lemma OAI.ElementaryPositivity.RawShuffle.unitalSourceFiltration_translation_mem line 98
  7. lemma OAI.ElementaryPositivity.RawShuffle.unitalSourceTensorFiltration_translateLeft line 111
  8. def OAI.ElementaryPositivity.RawShuffle.unitalRestrictionRelativeB line 128
  9. lemma OAI.ElementaryPositivity.RawShuffle.unitalRestrictionRelativeB_coeff_filtration line 133
  10. def OAI.ElementaryPositivity.RawShuffle.unitalSourceTensorFiltrationIdeal line 146
  11. def OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.unitalSeparationSeries line 152
  12. lemma OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.unitalSeparationSeries_coeff_filtration line 158
  13. lemma OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.quotientInverseKernelUnit_zero_left line 172
  14. lemma OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.quotientInverseKernelUnit_zero_right line 175
  15. lemma OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.unitalSeparationSeries_coeff_positive_next line 179