OAI/Combinatorics/Progressions/Geometry/MixedReplicatedCoordinates.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.MixedReplicatedIndex line 10
  2. def OAI.Erdos3.mixedHead line 12
  3. def OAI.Erdos3.mixedReplica line 14
  4. theorem OAI.Erdos3.mixedReplica_injective line 16
  5. theorem OAI.Erdos3.mixedReplicated_cases line 20
  6. def OAI.Erdos3.mixedRepeatedCoordinates line 31
  7. theorem OAI.Erdos3.mixedRepeatedCoordinates_length line 34
  8. theorem OAI.Erdos3.mixedRepeatedCoordinates_nodup line 37
  9. theorem OAI.Erdos3.mixedRepeatedCoordinates_get line 40
  10. theorem OAI.Erdos3.mem_mixedRepeatedCoordinates line 44
  11. def OAI.Erdos3.mixedReplicatedInput line 56
  12. theorem OAI.Erdos3.mixedReplicatedInput_head line 63
  13. theorem OAI.Erdos3.mixedReplicatedInput_replica line 66
  14. theorem OAI.Erdos3.mixedReplicatedInput_diagonal line 69