lean_workbook_plus_14096
ProvedDenote , , , so we have .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14096 (x y z t a b c d : ℝ) (h₁ : x ≠ 0 ∧ y ≠ 0 ∧ z ≠ 0 ∧ t ≠ 0) (h₂ : a = y / x ∧ b = z / y ∧ c = t / z ∧ d = x / t) : a * b * c * d = 1 := by sorry
Source