[Imo2010P1] link to source

dwrensha · Nov 21, 2023 · e4095c8 · e4095c8
1 parent 4b190e5
commit e4095c8
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Compfiles/Imo2010P1.lean b/Compfiles/Imo2010P1.lean
@@ -25,6 +25,8 @@ determine solution_set : Set (ℝ → ℝ) :=
 
 problem imo2010_p1 (f : ℝ → ℝ) :
     f ∈ solution_set ↔ ∀ x y, f (⌊x⌋ * y) = f x * ⌊f y⌋ :=
+  -- Solution adapted from
+  -- https://github.com/mortarsanjaya/imo-A-and-N/blob/main/src/IMO2010/A1/A1.lean
 ---- `→`
 ⟨λ h x y ↦ h.elim
   (λ h ↦ Exists.elim h $ λ C h ↦ h.2.symm ▸ h.1.symm ▸