lean_workbook_plus_39404

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

If $x$ and $y$ are real numbers such that $x^2+y^2=1$ , find minimum and maximum of $xy(y^2-x^2)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_39404 (x y : ℝ) (h : x ^ 2 + y ^ 2 = 1) :
  -1 ≤ x * y * (y ^ 2 - x ^ 2) ∧ x * y * (y ^ 2 - x ^ 2) ≤ 1   :=  by sorry

Source