lean_workbook_plus_7000

Proved

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

If $abc=1$ and $a=\frac{x}{y} , b=\frac{y}{z}$ we obtain: $\frac{x}{y}\cdot\frac{y}{z}\cdot c=1,$ which gives $c=\frac{z}{x}.$ \nHence, if $abc=1$ we can always say that $a=\frac{x}{y}$ , $b=\frac{y}{z}$ and $c=\frac{z}{x}$ for $xyz\neq0.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7000  (x y z : ℝ)
  (a b c : ℝ)
  (h₀ : x ≠ 0 ∧ y ≠ 0 ∧ z ≠ 0)
  (h₁ : a ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0)
  (h₂ : a * b * c = 1)
  (h₃ : a = x / y)
  (h₄ : b = y / z)
  (h₅ : c = z / x) :
  x / y * (y / z) * (z / x) = 1   :=  by sorry

Source

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

View graph