lean_workbook_plus_57913
ProvedGiven a set of distinct positive integers, none of which has a prime divisor greater than , prove that contains a subset of elements whose product is the th power of an integer.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_57913 (M : Finset ℕ) (Mpos : ∀ m ∈ M, 0 < m)
(Mdivisors : ∀ m ∈ M, ∀ n, m.Prime ∧ n ∣ m → m ≤ 23)
: ∃ M' : Finset ℕ, M' ⊆ M ∧ ∃ k, M'.prod id = k^4 := by sorrySource