OAI/NumberTheory/CubicGram/PrimeFactors.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Squarefree factorization and exact prime detector products.

  1. def OAI.CubicFirstMoment.primeFactors line 15
  2. lemma OAI.CubicFirstMoment.primeFactors_nodup line 17
  3. lemma OAI.CubicFirstMoment.primeFactors_norm_prod line 21
  4. lemma OAI.CubicFirstMoment.primeFactors_norm_prod_real line 28
  5. lemma OAI.CubicFirstMoment.prime_iff_primeFactors_card_one line 33
  6. def OAI.CubicFirstMoment.roughProduct line 47
  7. lemma OAI.CubicFirstMoment.primeFactor_norm_pos line 50
  8. lemma OAI.CubicFirstMoment.roughProduct_of_prime line 55
  9. lemma OAI.CubicFirstMoment.roughProduct_eq_zero_of_three_factors line 65
  10. lemma OAI.CubicFirstMoment.exact_prime_detector line 83
  11. lemma OAI.CubicFirstMoment.roughProduct_distinguished_subsets line 109