Product_of_Division_Products
Proveddivisionproofwikirings
Let R be a commutative ring with unity. Then (a/c) * (b/d) = (ab)/(cd).
Preamble
import Mathlib.Algebra.Field.Basic
Formal statement
theorem Product_of_Division_Products {F : Type _} [Field F] (a b c d : F) (hc : c ≠ 0) (hd : d ≠ 0) : (a / c) * (b / d) = (a * b) / (c * d) := by sorrySource