Equality_of_Division_Products_v2
Proveddivisionproofwikirings
Let R be a commutative ring with unity. Then a/c = b/d iff ad = bc.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Equality_of_Division_Products_v2 {F : Type _} [Field F] (a b c d : F) (hc : c ≠ 0) (hd : d ≠ 0) : a / c = b / d ↔ a * d = b * c := by sorrySource