Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1990P4

module

public import Mathlib.Tactic
public import Mathlib.Algebra.Order.Positive.Field
public import Mathlib.Data.Set.Card.Arithmetic
public import Mathlib.Algebra.Ring.BooleanRing
public import Mathlib.Algebra.Algebra.Hom.Rat

public section


/-!
# International Mathematical Olympiad 1990, Problem 4

Let $\mathbb{Q^+}$ be the set of positive rational numbers.
Construct a function $f :\mathbb{Q^+}\rightarrow\mathbb{Q^+}$ such that $f(xf(y)) = \frac{f(x)}{y}$ for all $x, y\in\mathbb{Q^+}$.
-/

namespace Imo1990P4

abbrev PRat := { q : ℚ // 0 < q }

notation "ℚ+" => PRat


noncomputable /- determine -/ abbrev f : ℚ+ → ℚ+ := sorry

theorem imo1990_p4 (x y : ℚ+) : f (x * f y) = f x / y := sorry


end Imo1990P4

File author(s): Constantin Seebach

This problem has a complete formalized solution.