lean_workbook_plus_32045

Proved

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

If $a\\cdot\\frac{1}{b}=1, b\\cdot\\frac{1}{c}=1$ , then $c\\cdot\\frac{1}{a}=1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_32045 (a b c : ℝ) (h₁ : a * (1/b) = 1) (h₂ : b * (1/c) = 1) : c * (1/a) = 1   :=  by sorry

Source