lean_workbook_plus_41357

Open

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

Prove the trigonometric identity: $\tan(x) = \frac{\sin(x)}{\cos(x)}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_41357 (x : ℝ) : tan x = sin x / cos x   :=  by sorry

Source