lean_workbook_plus_7134

Proved

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

The term can be written in the form $\frac{2(1+x^2y^2)}{xy}=2\left(\frac{1}{xy}+xy\right)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7134 (x y : ℝ) : 2 * (1 + x^2 * y^2) / (x * y) = 2 * (1 / (x * y) + x * y)   :=  by sorry

Source