OAI/Combinatorics/Chromatic/Walls/SquarefreeBlocks.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.SquarefreeBlocks.target line 13
  2. def OAI.ElementaryPositivity.SquarefreeBlocks.vector line 15
  3. lemma OAI.ElementaryPositivity.SquarefreeBlocks.target_apply line 17
  4. lemma OAI.ElementaryPositivity.SquarefreeBlocks.vector_apply line 33
  5. lemma OAI.ElementaryPositivity.SquarefreeBlocks.membership_unique line 39
  6. lemma OAI.ElementaryPositivity.SquarefreeBlocks.membership_range line 53
  7. def OAI.ElementaryPositivity.SquarefreeBlocks.coloring line 64
  8. lemma OAI.ElementaryPositivity.SquarefreeBlocks.coloring_mem line 66
  9. lemma OAI.ElementaryPositivity.SquarefreeBlocks.coloring_eq line 68
  10. def OAI.ElementaryPositivity.SquarefreeBlocks.blocks line 71
  11. lemma OAI.ElementaryPositivity.SquarefreeBlocks.mem_blocks line 74
  12. lemma OAI.ElementaryPositivity.SquarefreeBlocks.blocks_vector line 76
  13. def OAI.ElementaryPositivity.SquarefreeBlocks.equiv line 85