OAI/Combinatorics/Chromatic/Shuffle/UnitalFiltration.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RawShuffle.unitalSourceFiltration line 13
2. lemma OAI.ElementaryPositivity.RawShuffle.unitalSourceFiltration_nonzero line 18
3. lemma OAI.ElementaryPositivity.RawShuffle.castB_mem_unitalSourceFiltration line 23
4. lemma OAI.ElementaryPositivity.RawShuffle.unitalSourceFiltration_unit line 30
5. lemma OAI.ElementaryPositivity.RawShuffle.unitalSourceFiltration_mul_mem line 34
6. lemma OAI.ElementaryPositivity.RawShuffle.unitalSourceFiltration_antitone line 47
7. def OAI.ElementaryPositivity.RawShuffle.unitalSourceTensorFiltration line 59
8. lemma OAI.ElementaryPositivity.RawShuffle.unitalSourceTensorFiltration_nonzero line 64
9. lemma OAI.ElementaryPositivity.RawShuffle.restrictionBUnit_independent line 72
10. lemma OAI.ElementaryPositivity.RawShuffle.restrictionBUnit_unitalSourceTensorFiltration line 79
11. lemma OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.inverseKernelUnit_zero_left line 130
12. lemma OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.inverseKernelUnit_zero_right line 138
13. lemma OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.braidingRatioUnit_zero_left line 146
14. lemma OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.braidingRatioUnit_zero_right line 151
15. lemma OAI.ElementaryPositivity.RawShuffle.braidingDifference_coeff_mul_next line 157
16. lemma OAI.ElementaryPositivity.RawShuffle.braidingDifference_coeff_mul_unital_next line 174