OAI/Combinatorics/Progressions/Lattices/AllocatedSupportedSlicedResidue.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.containedSupportedProgressionLaw_residue_support line 25
  2. theorem OAI.Erdos3.containedSupportedProgressionLaw_residue_eq line 42
  3. theorem OAI.Erdos3.containedSupportedProgressionAxisLaw_fiberLaw line 49
  4. theorem OAI.Erdos3.containedSupportedProgressionAxisLaw_residue_support line 56
  5. theorem OAI.Erdos3.containedSupportedProgressionAxisLaw_residue_eq line 67
  6. theorem OAI.Erdos3.integerProgressionSupport_subset_iff_fin line 85
  7. theorem OAI.Erdos3.integerProgressionSupport_subset_of_fin line 110
  8. def OAI.Erdos3.finIntegerIntervalEquiv line 116
  9. def OAI.Erdos3.zeroScalarFinPoint line 126
  10. theorem OAI.Erdos3.zeroScalar_fin_mean line 129
  11. theorem OAI.Erdos3.zeroScalar_fin_complexMean line 146
  12. theorem OAI.Erdos3.integerScalarCubeWeights_pi_fin_complexMean line 158
  13. def OAI.Erdos3.principalFinTuplePoint line 177
  14. theorem OAI.Erdos3.principalTupleWeights_fin_complexMean line 180
  15. theorem OAI.Erdos3.principalTupleWeights_fin_mean line 185
  16. def OAI.Erdos3.principalFinResidueLabel line 194
  17. def OAI.Erdos3.principalFinResidueCell line 197
  18. theorem OAI.Erdos3.principalFinTuplePoint_residue line 203
  19. theorem OAI.Erdos3.principalFinResidueCell_mass line 211
  20. theorem OAI.Erdos3.containedProgressionTupleMap_finPoint line 232
  21. theorem OAI.Erdos3.principalAffineIntervalLaw_eq_contained line 251
  22. theorem OAI.Erdos3.containedSupportedProgressionLaw_fin_condition_mean line 270
  23. theorem OAI.Erdos3.containedSupportedProgressionLaw_fin_condition_complexMean line 293
  24. theorem OAI.Erdos3.containedSupportedProgressionLaw_eq_fin_condition line 313
  25. theorem OAI.Erdos3.principalAffineIntervalPoint_residue line 338
  26. theorem OAI.Erdos3.principalAffineIntervalLaw_partition_complexMean line 365
  27. theorem OAI.Erdos3.principalAffineIntervalAxisLaw_complexMean_restricted line 408
  28. theorem OAI.Erdos3.principalAffineIntervalAxisLaw_eq_restricted line 419
  29. theorem OAI.Erdos3.principalAffineIntervalLaw_axis_complexMean line 434
  30. theorem OAI.Erdos3.principalAffineIntervalLaw_axis_contained_complexMean line 446
  31. theorem OAI.Erdos3.VectorPolynomial.allocatedLongResidueWeights_support_label line 502
  32. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedLongResidueReference line 513
  33. theorem OAI.Erdos3.VectorPolynomial.allocatedNonkernelJetMatrix_residue_of_label line 545
  34. theorem OAI.Erdos3.VectorPolynomial.allocatedLongResidueWeights_reference_matrix line 557
  35. theorem OAI.Erdos3.VectorPolynomial.allocatedNonkernelJetMatrix_residue_both line 608
  36. theorem OAI.Erdos3.VectorPolynomial.allocatedPartitionedJetMatrix_residue_both line 618
  37. theorem OAI.Erdos3.VectorPolynomial.allocatedPartitionedJetMatrix_image_eq_of_residue_both line 630
  38. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalDeckJet_law_eq_of_residue_both line 640
  39. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedSlicedNonkernel_residue_constant line 698
  40. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedSlicedDeck_law_constant line 707