Addition_of_Division_Products_v2
Proveddivisionproofwikirings
Let R be a commutative ring with unity. Then a/c + b/d = (ad + bc)/(c*d).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Addition_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) / (c * d) := by sorrySource