OAI/Combinatorics/Progressions/Lattices/AffineCoefficientResidueWidths.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.integerContractedRow_monomial line 15
  2. theorem OAI.Erdos3.VectorPolynomial.exists_unit_integer_mode_rows line 20
  3. theorem OAI.Erdos3.VectorPolynomial.layeredModeTestedPhase_empty_zero line 46
  4. theorem OAI.Erdos3.VectorPolynomial.exists_affine_coefficient_local_removal line 54
  5. theorem OAI.Erdos3.VectorPolynomial.affine_coefficient_mode_residue_removal_lipschitz_amplitude line 136
  6. theorem OAI.Erdos3.VectorPolynomial.affine_coefficient_mode_residue_removal line 198
  7. theorem OAI.Erdos3.VectorPolynomial.anchored_affine_coefficient_mode_residue_removal line 257
  8. def OAI.Erdos3.VectorPolynomial.affineCoefficientModeTrivial line 317
  9. theorem OAI.Erdos3.VectorPolynomial.not_affineCoefficientModeTrivial_iff line 325
  10. theorem OAI.Erdos3.VectorPolynomial.affineModeLift_zero_of_homogeneous line 335
  11. theorem OAI.Erdos3.VectorPolynomial.layeredCoefficientCharacter_eq_one_of_trivial line 345
  12. theorem OAI.Erdos3.VectorPolynomial.affine_coefficient_residue_removal_of_widths_lipschitz_amplitude line 380
  13. theorem OAI.Erdos3.VectorPolynomial.affine_coefficient_residue_removal_of_widths line 471