lean_workbook_plus_79537

Proved

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

proofwiki

$\frac{GD}{AC}=\frac{BD}{AB} \rightarrow GD \cdot AB=BD \cdot AC$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_79537 {ac ab bd gd: ℝ} (h : ab ≠ 0 ∧ ac ≠ 0 ∧ bd ≠ 0 ∧ gd ≠ 0) : (gd/ac) = (bd/ab) → gd * ab = bd * ac   :=  by sorry

Source