OAI/Combinatorics/Chromatic/Shuffle/GlobalTensorDetection.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RawShuffle.globalTensorComponent line 14
2. lemma OAI.ElementaryPositivity.RawShuffle.globalComponent_lof_ne line 20
3. lemma OAI.ElementaryPositivity.RawShuffle.unitalSourceTensorGradeEquiv_symm_part line 26
4. lemma OAI.ElementaryPositivity.RawShuffle.globalTensorComponent_inclusion line 33
5. lemma OAI.ElementaryPositivity.RawShuffle.globalTensorGradeInclusion_injective line 51
6. lemma OAI.ElementaryPositivity.RawShuffle.globalTensorComponent_inclusion_ne_left line 60
7. lemma OAI.ElementaryPositivity.RawShuffle.globalTensorComponent_split_ne line 73
8. lemma OAI.ElementaryPositivity.RawShuffle.globalTensorComponent_coproduct line 83
9. lemma OAI.ElementaryPositivity.RawShuffle.globalComponent_unit line 108
10. lemma OAI.ElementaryPositivity.RawShuffle.globalPrimitive_split_zero line 113
11. lemma OAI.ElementaryPositivity.RawShuffle.globalPrimitive_iff_split_zero line 132