OAI/Combinatorics/Progressions/Estimates/ModularMultilinearSublevelFiber.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.zmod_affine_zero_card_le_gcd line 15
  2. theorem OAI.Erdos3.zmod_mul_zero_card_eq_gcd line 43
  3. theorem OAI.Erdos3.zmod_mul_zero_expect_eq_gcd line 49
  4. theorem OAI.Erdos3.zmod_affine_zero_expect_le_gcd line 57
  5. theorem OAI.Erdos3.zmod_affine_zero_conditional_expect_le_gcd line 67
  6. theorem OAI.Erdos3.zmod_gcd_expect_eq_mul_zero_expect line 75
  7. theorem OAI.Erdos3.zmod_prime_power_affine_zero_card_le line 83
  8. theorem OAI.Erdos3.zmod_prime_power_affine_zero_expect_le line 95
  9. theorem OAI.Erdos3.zmod_prime_power_affine_zero_expect_le_rpow line 114