lean_workbook_plus_35923
ProvedWhy does mean ?
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_35923 (a b c d : ℝ) (hb : b ≠ 0) (hd : d ≠ 0) : a / b = c / d ↔ a * d = b * c := by sorry
Source
Why does mean ?
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_35923 (a b c d : ℝ) (hb : b ≠ 0) (hd : d ≠ 0) : a / b = c / d ↔ a * d = b * c := by sorry