lean_workbook_plus_45624
ProvedSuppose is a prime with . Show that for any set of consecutive integers, the set cannot be divided two subsets so that the product of the members of the one set is equal to the product of the members of the other set.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_45624 (p : ℕ) (hp : p.Prime) (hp_mod_4_eq_3 : p ≡ 3 [ZMOD 4]) (A : Finset ℤ) (hA : A.card = p - 1) (hA_consecutive : ∀ a : ℤ, a ∈ A ∧ a + 1 ∈ A) : ¬ (∃ B C : Finset ℤ, B ∪ C = A ∧ B.prod id = C.prod id) := by sorry
Source