OAI/Combinatorics/Chromatic/Walls/TensorAssociatedGrade.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.LinearFiltration.gradeProjection line 12
  2. lemma OAI.ElementaryPositivity.LinearFiltration.gradeProjection_mem line 16
  3. lemma OAI.ElementaryPositivity.LinearFiltration.gradeProjection_zero line 22
  4. abbrev OAI.ElementaryPositivity.LinearFiltration.TensorGrade line 28
  5. def OAI.ElementaryPositivity.LinearFiltration.tensorGradeInclusion line 31
  6. lemma OAI.ElementaryPositivity.LinearFiltration.tensorGradeInclusion_mk line 41
  7. lemma OAI.ElementaryPositivity.LinearFiltration.tensorProjection_kills line 46
  8. def OAI.ElementaryPositivity.LinearFiltration.tensorGradeProjection line 59
  9. lemma OAI.ElementaryPositivity.LinearFiltration.tensorGradeProjection_mk line 67
  10. lemma OAI.ElementaryPositivity.LinearFiltration.tensorGradeProjection_inclusion_self line 72
  11. abbrev OAI.ElementaryPositivity.LinearFiltration.TensorGradePart line 85
  12. def OAI.ElementaryPositivity.LinearFiltration.tensorGradeInclusionW line 88
  13. lemma OAI.ElementaryPositivity.LinearFiltration.tensorGradeInclusionW_mk line 97
  14. def OAI.ElementaryPositivity.LinearFiltration.tensorGradeProjectionW line 102
  15. lemma OAI.ElementaryPositivity.LinearFiltration.tensorGradeProjectionW_mk line 113
  16. lemma OAI.ElementaryPositivity.LinearFiltration.tensorGradeProjectionW_inclusion_self line 118
  17. lemma OAI.ElementaryPositivity.LinearFiltration.tensorGradeProjectionW_inclusion_ne line 131
  18. def OAI.ElementaryPositivity.LinearFiltration.tensorGradeSum line 146
  19. lemma OAI.ElementaryPositivity.LinearFiltration.tensorGradeProjectionW_sum line 150
  20. lemma OAI.ElementaryPositivity.LinearFiltration.tensorGradeSum_injective line 171
  21. lemma OAI.ElementaryPositivity.LinearFiltration.tensorGradeSum_surjective line 179
  22. def OAI.ElementaryPositivity.LinearFiltration.tensorGradeEquiv line 209