lean_workbook_plus_40625

Open

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

Find the parameter equations for the ellipse $a^2 + 3b^2 = 1$ using $a=\cos \alpha$ and $b=\frac{\sin \alpha}{\sqrt{3}}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_40625 (a b : ℝ) (α : ℝ) (h₁ : a = Real.cos α) (h₂ : b = Real.sin α / Real.sqrt 3) : a^2 + 3 * b^2 = 1   :=  by sorry

Source