OAI/NumberTheory/Ostmann/Quadratic/KernelPairIdentification.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Disjoint prime supports identify a kernel pair from its product

  1. theorem OAI.Ostmann.cross_coprime_factor_unique line 14
  2. theorem OAI.Ostmann.signed_kernel_product_magnitudes line 24
  3. theorem OAI.Ostmann.kernel_product_fiber_card_le_two line 32

    Source documentation

    For any fixed signed product there are at most two pairs from two nonzero kernel families with disjoint prime supports.

    theorem kernel_product_fiber_card_le_two (A B : Finset ℤ) (d : ℤ)
    (hA : ∀ u ∈ A, u ≠ 0)
    (hAB : ∀ u ∈ A, ∀ v ∈ B, u.natAbs.Coprime v.natAbs) :
    Fintype.card {z : A × B // (z.1 : ℤ) * (z.2 : ℤ) = d} ≤ 2 := by
…