lean_workbook_plus_15004
ProvedLet be a set of integers, none of them are greater than . Prove that there exist such that product of all elements of is a square number.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_15004 (s : Finset ℤ) (hs : ∀ x ∈ s, 0 < x ∧ x ≤ 199) : ∃ t ⊆ s, ∃ z : ℤ, t.prod (fun x ↦ x) = z^2 := by sorry
Source