lean_workbook_plus_45463

Proved

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

$\frac{p_{1}}{p_{2}}+\frac{p_{2}}{p_{1}}=\frac{p_{1}^{2}+p_{2}^{2}}{p_{1}p_{2}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_45463 (p₁ p₂ : ℝ) : p₁ / p₂ + p₂ / p₁ = (p₁ ^ 2 + p₂ ^ 2) / (p₁ * p₂)   :=  by sorry

Source