OAI/NumberTheory/Ostmann/QuadraticCenter/HalfKernel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A small divisor carrying half the prime factors of a squarefree kernel

  1. theorem OAI.Ostmann.exists_half_subset_product line 12
  2. theorem OAI.Ostmann.squarefree_half_kernel line 40
  3. theorem OAI.Ostmann.half_kernel_weight line 57
  4. def OAI.Ostmann.smallHalfKernel line 65
  5. theorem OAI.Ostmann.smallHalfKernel_spec line 69