OAI/Combinatorics/Chromatic/Walls/UnitalGradeComparison.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.LinearFiltration.congr line 10
2. lemma OAI.ElementaryPositivity.LinearFiltration.congr_mk line 14
3. def OAI.ElementaryPositivity.RawShuffle.unitalGradeNonzeroEquiv line 24
4. lemma OAI.ElementaryPositivity.RawShuffle.unitalGradeNonzeroEquiv_mk line 28
5. def OAI.ElementaryPositivity.RawShuffle.unitalTensorGradeNonzeroEquiv line 33
6. lemma OAI.ElementaryPositivity.RawShuffle.unitalTensorGradeNonzeroEquiv_mk line 37
7. lemma OAI.ElementaryPositivity.RawShuffle.unitalGradeCoproduct_nonzero line 44
8. lemma OAI.ElementaryPositivity.RawShuffle.unitalGradeNonzeroEquiv_cast line 62