lean_workbook_plus_52387

Open

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

prove that $\sqrt{\frac{1+\frac{1}{\cos \theta}}{\frac{1}{\cos \theta}-1}} = \sqrt{\frac{\cos \theta +1}{1-\cos \theta}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_52387 (θ : ℝ) (h : cos θ ≠ 0) : √((1 + 1 / cos θ) / (1 / cos θ - 1)) = √((cos θ + 1) / (1 - cos θ))   :=  by sorry

Source