lean_workbook_plus_16631

Proved

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

Prove that $\frac{\sqrt{2s / a}}{\sqrt{2s / a'}} = \sqrt{\frac{2s / a}{2s / a'}} = \sqrt{\frac{a'}{a}}$ for positive $a, a', s$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_16631 (a a' s : ℝ) (ha : 0 < a) (ha' : 0 < a') (hs : 0 < s) : √((2 * s) / a) / √((2 * s) / a') = √(a' / a)   :=  by sorry

Source