lean_workbook_plus_46768
ProvedProve that $\sqrt{x} \cdot \sqrt{y} = \sqrt{xy}$ for positive real numbers x and y.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_46768 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : Real.sqrt x * Real.sqrt y = Real.sqrt (x * y) := by sorry
Source