lean_workbook_plus_53228

Proved

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

$\frac{1}{x^{2}}+\frac{1}{y^{2}}=\frac{1}{z^{2}}$ $\Rightarrow\left(xz\right)^{2}+\left(yz\right)^{2}=\left(xy\right)^{2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_53228 {x y z : ℚ} (h : x ≠ 0 ∧ y ≠ 0 ∧ z ≠ 0) (habc : x * y * z ≠ 0) (h : 1 / x ^ 2 + 1 / y ^ 2 = 1 / z ^ 2) : (x * z) ^ 2 + (y * z) ^ 2 = (x * y) ^ 2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph