OAI/Combinatorics/Progressions/Linear/AllocatedModularRankCongruenceOutput.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.canonicalRankBlockEmbedding line 16
  2. def OAI.Erdos3.canonicalRankBlock line 22
  3. theorem OAI.Erdos3.canonicalRankBlock_card line 26
  4. theorem OAI.Erdos3.mem_canonicalRankBlock line 30
  5. theorem OAI.Erdos3.canonicalRankBlock_pairwise_disjoint line 37
  6. theorem OAI.Erdos3.canonicalRankBlock_disjoint line 54
  7. theorem OAI.Erdos3.principalCoefficientSlot_eq_block_sum line 63
  8. theorem OAI.Erdos3.principalCoefficientSlot_monomial line 70
  9. theorem OAI.Erdos3.principalCoefficientSlot_squarefree line 77
  10. theorem OAI.Erdos3.principalCoefficientSlot_eq_squarefree line 86
  11. def OAI.Erdos3.VectorPolynomial.allocatedRankBlockEmbedding line 100
  12. def OAI.Erdos3.VectorPolynomial.allocatedRankBlock line 104
  13. def OAI.Erdos3.VectorPolynomial.allocatedRankSelected line 108
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedRankSelected_mem line 112
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedRankBlock_pairwise_disjoint line 116
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedRankBlock_card line 122
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedRankBlock_disjoint line 126
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedRankBlock_monomial line 131
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedRankBlock_monomial_smul line 138
  20. def OAI.Erdos3.kernelRankBlockEmbedding line 159
  21. theorem OAI.Erdos3.kernelRankBlockEmbedding_apply line 166
  22. def OAI.Erdos3.kernelRankBlock line 170
  23. theorem OAI.Erdos3.kernelRankBlock_eq_image line 174
  24. theorem OAI.Erdos3.kernelRankBlock_card line 180
  25. theorem OAI.Erdos3.mem_kernelRankBlock line 184
  26. theorem OAI.Erdos3.kernelRankBlock_pairwise_disjoint line 191
  27. theorem OAI.Erdos3.kernelRankBlock_disjoint_canonicalRankBlock line 201
  28. def OAI.Erdos3.kernelRankCoefficientSlot line 210
  29. theorem OAI.Erdos3.kernelRankCoefficientSlot_degree line 216
  30. theorem OAI.Erdos3.kernelRankCoefficientSlot_eq_block_sum line 221
  31. theorem OAI.Erdos3.kernelRankCoefficientSlot_apply line 228
  32. theorem OAI.Erdos3.kernelRankCoefficientSlot_injective line 236
  33. theorem OAI.Erdos3.kernelRankCoefficientSlot_monomial line 246
  34. theorem OAI.Erdos3.kernelRankCoefficientSlot_squarefree line 254
  35. theorem OAI.Erdos3.kernelRankCoefficientSlot_eq_squarefree line 262
  36. theorem OAI.Erdos3.exists_kernelRankEmbedding line 271
  37. def OAI.Erdos3.kernelRankEmbeddingOfCapacity line 276
  38. abbrev OAI.Erdos3.SamplerLongVariables line 293
  39. def OAI.Erdos3.samplerLongEmbedding line 297
  40. theorem OAI.Erdos3.samplerLongEmbedding_common line 303
  41. theorem OAI.Erdos3.samplerLongEmbedding_dedicated line 306
  42. theorem OAI.Erdos3.samplerLongEmbedding_common_mem_range line 311
  43. theorem OAI.Erdos3.samplerLongEmbedding_dedicated_mem_range line 315
  44. theorem OAI.Erdos3.samplerLongEmbedding_block line 328
  45. theorem OAI.Erdos3.samplerLongEmbedding_principalExponent line 336
  46. theorem OAI.Erdos3.homogeneousComponent_killCompl line 348
  47. theorem OAI.Erdos3.homogeneousComponent_polynomialTranslate_top line 354
  48. theorem OAI.Erdos3.homogeneousComponent_restricted_translate_top line 363
  49. theorem OAI.Erdos3.homogeneousComponent_conditionPolynomial_top line 370
  50. theorem OAI.Erdos3.samplerLong_principal_coefficient line 379
  51. abbrev OAI.Erdos3.VectorPolynomial.LayerSamplerLongVariables line 396
  52. def OAI.Erdos3.VectorPolynomial.allocatedLongEmbedding line 400
  53. theorem OAI.Erdos3.VectorPolynomial.allocatedLong_top_independent line 404
  54. theorem OAI.Erdos3.VectorPolynomial.allocatedLong_top_origin_independent line 416
  55. theorem OAI.Erdos3.VectorPolynomial.allocatedLongEmbedding_block line 427
  56. theorem OAI.Erdos3.VectorPolynomial.allocatedLong_principal_coefficient line 434
  57. abbrev OAI.Erdos3.VectorPolynomial.AllocatedDegreeActiveAxis line 459
  58. abbrev OAI.Erdos3.VectorPolynomial.AllocatedDegreeRankOutput line 462
  59. def OAI.Erdos3.VectorPolynomial.allocatedDegreeLongAxis line 466
  60. def OAI.Erdos3.VectorPolynomial.allocatedDegreeRankBlock line 470
  61. theorem OAI.Erdos3.VectorPolynomial.allocatedDegreeRankBlock_card line 479
  62. theorem OAI.Erdos3.VectorPolynomial.allocatedDegreeRankBlock_disjoint line 488
  63. def OAI.Erdos3.VectorPolynomial.allocatedDegreeRankSelected line 500
  64. theorem OAI.Erdos3.VectorPolynomial.allocatedDegreeRankSelected_mem line 507
  65. theorem OAI.Erdos3.VectorPolynomial.allocatedDegreeRankBlock_deck_projection_disjoint line 517
  66. theorem OAI.Erdos3.VectorPolynomial.allocatedDegreeRankOutput_card_le line 526
  67. def OAI.Erdos3.canonicalPrincipalSubblockSlot line 550
  68. theorem OAI.Erdos3.canonicalPrincipalSubblockSlot_injective line 556
  69. theorem OAI.Erdos3.canonicalPrincipalSubblockSlot_degree line 562
  70. def OAI.Erdos3.canonicalSelectedTopResidual line 567
  71. theorem OAI.Erdos3.canonicalBoundedCoefficient_selected_top line 574
  72. theorem OAI.Erdos3.samplerLong_killCompl_principal_monomial line 592
  73. def OAI.Erdos3.canonicalSelectedLongTopResidual line 601
  74. theorem OAI.Erdos3.canonicalBoundedCoefficient_selected_long_top line 608
  75. theorem OAI.Erdos3.canonicalBoundedInteger_selected_long_top line 637
  76. theorem OAI.Erdos3.VectorPolynomial.allocatedBoundedCoefficient_selected_long_top line 672
  77. abbrev OAI.Erdos3.VectorPolynomial.SpatialDegreeOutput line 704
  78. abbrev OAI.Erdos3.VectorPolynomial.AllocatedTaggedRankOutput line 706
  79. def OAI.Erdos3.VectorPolynomial.allocatedSpatialRankBlock line 710
  80. def OAI.Erdos3.VectorPolynomial.allocatedTaggedRankBlock line 715
  81. theorem OAI.Erdos3.VectorPolynomial.allocatedTaggedRankBlock_card line 723
  82. theorem OAI.Erdos3.VectorPolynomial.allocatedTaggedRankBlock_disjoint line 733
  83. def OAI.Erdos3.VectorPolynomial.allocatedTaggedRankSelected line 746
  84. theorem OAI.Erdos3.VectorPolynomial.allocatedTaggedRankSelected_mem line 753
  85. theorem OAI.Erdos3.VectorPolynomial.allocatedSpatialRankBlock_product line 763
  86. theorem OAI.Erdos3.VectorPolynomial.spatialDegreeOutput_card line 770
  87. theorem OAI.Erdos3.VectorPolynomial.allocatedTaggedRankOutput_card_le line 776
  88. theorem OAI.Erdos3.VectorPolynomial.spatialDegreeOutput_sum_card line 785
  89. theorem OAI.Erdos3.VectorPolynomial.allocatedTaggedRankOutput_sum_card_le line 795
  90. abbrev OAI.Erdos3.VectorPolynomial.AllocatedCongruenceIntegerAxis line 818
  91. abbrev OAI.Erdos3.VectorPolynomial.AllocatedCongruenceRankOutput line 821
  92. def OAI.Erdos3.VectorPolynomial.allocatedCongruenceIntegerEmbedding line 825
  93. def OAI.Erdos3.VectorPolynomial.allocatedCongruenceOutputEmbedding line 833
  94. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceOutputEmbedding_spatial line 839
  95. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceOutputEmbedding_deck line 843
  96. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceOutputEmbedding_integer line 847
  97. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceRankOutput_card_le line 852
  98. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceRankOutput_sum_card_le line 864
  99. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceRankOutput_sum_card_le_uniform line 874
  100. theorem OAI.Erdos3.VectorPolynomial.preparedCongruenceRankOutput_sum_card_le line 884
  101. theorem OAI.Erdos3.VectorPolynomial.preparedCongruenceRankOutput_sum_card_fin_le line 901