Real_Multiplication_Distributes_over_Addition
Proveddistributivityproofwikireal-multiplication
The operation of multiplication on the set of real numbers R distributes over addition.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Real_Multiplication_Distributes_over_Addition (x y z : ℝ) : x * (y + z) = x * y + x * z := by sorry
Source