diff --git a/Compfiles/Imo2010P3.lean b/Compfiles/Imo2010P3.lean index c43e1aff..34233766 100644 --- a/Compfiles/Imo2010P3.lean +++ b/Compfiles/Imo2010P3.lean @@ -26,8 +26,13 @@ abbrev PosInt : Type := { x : ℤ // 0 < x } notation "ℤ>0" => PosInt -determine solution_set : Set (ℤ>0 → ℤ>0) := sorry +determine solution_set : Set (ℤ>0 → ℤ>0) := { f | f = id ∨ ∃ c, ∀ x, f x = x + c } + problem imo2010_p3 (g : ℤ>0 → ℤ>0) : g ∈ solution_set ↔ ∀ m n, IsSquare ((g m + n) * (g n + m)) := by - sorry + constructor + · rintro (rfl | ⟨c, hc⟩) m n + · use m + n; rw [id, id]; ac_rfl + · use m + n + c; rw [hc m, hc n]; ac_rfl + · sorry