Compfiles: Catalog Of Math Problems Formalized In Lean

Singapore2019P2


import Mathlib

/-!
# Singapore Math Olympiad (Senior) 2019 (Round 1), Problem 2

http://www.realsutra.com/limjeck/SMO_Senior_2019.pdf

Simplify $(sqrt{10} - sqrt{2})^{1/3} * (sqrt{10} + sqrt{2})^{7/3}$.
-/
open Real

namespace Singapore2019R1P2

noncomputable /- determine -/ abbrev solution : ℝ := sorry

theorem singapore2019_r1_p2 : (√10 - √2)^(1 / 3 : ℝ) * (√10 + √2)^(7 / 3 : ℝ) = solution := sorry

This problem has a complete formalized solution.

Open with the in-brower editor at live.lean-lang.org: