OAI/NumberTheory/GaussianMoat/SignedArithmetic.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianMoat.PrimitiveDirection line 9
  2. theorem OAI.GaussianMoat.int_multiple_of_determinant_zero line 11
  3. theorem OAI.GaussianMoat.exists_primitive_direction line 24
  4. theorem OAI.GaussianMoat.norm_dvd_norm line 35
  5. theorem OAI.GaussianMoat.factor_dvd_integer_iff line 40
  6. theorem OAI.GaussianMoat.not_both_factors_dvd_primitive line 57
  7. def OAI.GaussianMoat.signedFactor line 90
  8. theorem OAI.GaussianMoat.signedFactor_norm line 92
  9. theorem OAI.GaussianMoat.signedFactor_irreducible line 95
  10. theorem OAI.GaussianMoat.coprime_factors_of_norm_primes line 101
  11. theorem OAI.GaussianMoat.norm_finset_prod line 116
  12. theorem OAI.GaussianMoat.SplitSieve.prod_factors_dvd line 123
  13. theorem OAI.GaussianMoat.SplitSieve.eligible_product_le_norm line 133
  14. theorem OAI.GaussianMoat.SplitSieve.uneligible_product_dvd_coefficient line 146
  15. theorem OAI.GaussianMoat.SplitSieve.line_witness_norm_lower line 170