SixPrimeSquareClasses.lean

theorem dvd_sixPrimeProduct_of_squarefree_support
    (n : ℕ) (hn : Squarefree n)
    (hSupport : ∀ p : ℕ, p.Prime → p ∣ n → p ∈ ({3, 5, 7, 11, 13, 17} : Finset ℕ)) :
    n ∣ 255255

theorem three_negative_primes_squareClass
    (s : Finset ℕ) (hs : s ⊆ {3, 7, 11}) (hMod : (∏ p ∈ s, p) % 4 = 1) :
    ∃ t : Finset ℕ, t ⊆ {21, 33} ∧
      ∃ q : ℚ, q ≠ 0 ∧ (∏ p ∈ s, (p : ℚ)) = (∏ r ∈ t, (r : ℚ)) * q ^ 2

theorem exists_five_generator_squareClass_of_support
    (n : ℕ) (hn : Squarefree n)
    (hSupport : ∀ p : ℕ, p.Prime → p ∣ n → p ∈ ({3, 5, 7, 11, 13, 17} : Finset ℕ))
    (hMod : n % 4 = 1) :
    ∃ s : Finset ℕ, s ⊆ {5, 13, 17, 21, 33} ∧
      ∃ q : ℚ, q ≠ 0 ∧ (n : ℚ) = (∏ r ∈ s, (r : ℚ)) * q ^ 2

theorem exists_five_generator_squareClass_of_int_support
    (d : ℤ) (hdNonneg : 0 ≤ d) (hd : Squarefree d.natAbs)
    (hSupport : ∀ p : ℕ, p.Prime → (p : ℤ) ∣ d →
      p ∈ ({3, 5, 7, 11, 13, 17} : Finset ℕ))
    (hMod : d % 4 = 1) :
    ∃ s : Finset ℕ, s ⊆ {5, 13, 17, 21, 33} ∧
      ∃ q : ℚ, q ≠ 0 ∧ (d : ℚ) = (∏ r ∈ s, (r : ℚ)) * q ^ 2