OAI/Combinatorics/Chromatic/Shuffle/UnitalCoproductCoassociative.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.TensorTransport.assoc_sub_symm line 12
2. lemma OAI.ElementaryPositivity.RawShuffle.unitalSeparationConstant_eq_linear line 34
3. theorem OAI.ElementaryPositivity.RawShuffle.unitalCoproduct_coassoc_filtration line 44
4. lemma OAI.ElementaryPositivity.RawShuffle.unitalSeparationConstant_filtered line 114
5. def OAI.ElementaryPositivity.RawShuffle.unitalTensorCoproductLeft line 122
6. def OAI.ElementaryPositivity.RawShuffle.unitalTensorCoproductRight line 134
7. theorem OAI.ElementaryPositivity.RawShuffle.unitalGradeCoproduct_coassociative line 146