OAI/Combinatorics/Progressions/Estimates/CommonFixedNativeSquareFamily.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.UniformNativeBiasedSquareSpec line 15
  2. theorem OAI.Erdos3.exists_uniform_native_biased_square line 58
  3. def OAI.Erdos3.CommonNativeSquareFamilySpec line 149
  4. theorem OAI.Erdos3.exists_common_native_square_family line 200
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.HasNativeFactoredSquareInModel.mono line 251
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.HasNativeFactoredSquareInModel.rescale line 269
  7. def OAI.Erdos3.InductiveNativeSquareFamilySpec line 289
  8. theorem OAI.Erdos3.exists_inductive_native_square_family line 341
  9. theorem OAI.Erdos3.exists_stepTwo_native_square_family line 410
  10. def OAI.Erdos3.CommonFixedNativeSquareFamilySpec line 427
  11. theorem OAI.Erdos3.exists_common_fixed_native_square_family line 493
  12. theorem OAI.Erdos3.exists_stepTwo_common_fixed_square_family line 564