OAI/Combinatorics/Progressions/Linear/RankPreparationPaddedFreezingLifts.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.RankPreparationFamily.pad_polynomial line 14
  2. theorem OAI.Erdos3.RankPreparationFamily.pad_identity line 21
  3. def OAI.Erdos3.RankPreparationFamily.padCoordInclusion line 27
  4. theorem OAI.Erdos3.RankPreparationFamily.padCoord_isLt line 32
  5. def OAI.Erdos3.RankPreparationFamily.padCoordRestriction line 39
  6. theorem OAI.Erdos3.RankPreparationFamily.padCoordRestriction_inclusion line 44
  7. theorem OAI.Erdos3.RankPreparationFamily.padCoordInclusion_restriction line 53
  8. def OAI.Erdos3.RankPreparationFamily.padCoordEquiv line 62
  9. theorem OAI.Erdos3.RankPreparationFamily.label_cast line 69
  10. theorem OAI.Erdos3.RankPreparationFamily.eval_cast line 74
  11. theorem OAI.Erdos3.RankPreparationFamily.coefficients_cast line 80
  12. theorem OAI.Erdos3.RankPreparationFamily.padCoordInclusion_label line 87
  13. theorem OAI.Erdos3.RankPreparationFamily.padCoordEquiv_index line 92
  14. theorem OAI.Erdos3.RankPreparationFamily.padCoordEquiv_label line 95
  15. theorem OAI.Erdos3.RankPreparationFamily.padCoordInclusion_eval line 102
  16. theorem OAI.Erdos3.RankPreparationFamily.padCoordEquiv_eval line 108
  17. theorem OAI.Erdos3.RankPreparationFamily.padCoordInclusion_coefficients line 116
  18. theorem OAI.Erdos3.RankPreparationFamily.padCoordEquiv_coefficients line 122
  19. theorem OAI.Erdos3.RankPreparationFamily.pad_coordinateCopySum line 130
  20. theorem OAI.Erdos3.RankPreparationFamily.pad_coordinateCopySum_family line 141
  21. theorem OAI.Erdos3.RankPreparationFamily.pad_integerRemainder line 150
  22. def OAI.Erdos3.RankPreparationFamily.unpadCenter line 170
  23. theorem OAI.Erdos3.RankPreparationFamily.unpadCenter_equiv line 174
  24. theorem OAI.Erdos3.RankPreparationFamily.space_cast line 181
  25. theorem OAI.Erdos3.RankPreparationFamily.unpadCenter_mem line 187
  26. def OAI.Erdos3.RankPreparationFamily.padFullTaggedEquiv line 192
  27. theorem OAI.Erdos3.RankPreparationFamily.padFullTaggedEquiv_weight line 196
  28. theorem OAI.Erdos3.RankPreparationFamily.pad_fullTaggedPhysicalIntegerPoint line 206
  29. theorem OAI.Erdos3.RankPreparationFamily.pad_fullTaggedPhysicalIntegerPoint_restrict line 222
  30. theorem OAI.Erdos3.RankPreparationFamily.pad_fullTagged_observer line 231
  31. def OAI.Erdos3.RankPreparationFamily.padLowTaggedEquiv line 240
  32. theorem OAI.Erdos3.RankPreparationFamily.pad_lowTagged_card line 247
  33. def OAI.Erdos3.RankPreparationFamily.unpadFreezingLifts line 266
  34. theorem OAI.Erdos3.RankPreparationFamily.unpadFreezingLifts_degree line 271
  35. theorem OAI.Erdos3.RankPreparationFamily.unpadFreezingLifts_bound line 278
  36. theorem OAI.Erdos3.RankPreparationFamily.exists_unpadded_freezing_lifts line 296
  37. theorem OAI.Erdos3.RankPreparationFamily.pad_coordinateWeighted_sum line 313