All-Russian Regional Preparation NT Exercise 3

Let there be $4$ positive integers such that each is divisible by the **gcd** and divides the **lcm** of the other three. Show that their product is a perfect square.

Replace sorry in the template below with your solution. Mathlib version used by the checker is v4.29.0.

import Mathlib.Algebra.BigOperators.Group.Multiset.Defs
import Mathlib.Algebra.GCDMonoid.Multiset
import Mathlib.Algebra.GCDMonoid.Nat

theorem solution (s : Multiset ℕ) (h1 : s.card = 4) (h2 : ∀ x ∈ s, 0 < x)
    (h3 : ∀ x ∈ s, (s.erase x).gcd ∣ x) (h4 : ∀ x ∈ s, x ∣ (s.erase x).lcm) :
    ∃ m, s.prod = m ^ 2 := sorry

Submit Solution

Login to submit a solution.

Recent Submissions