Real_Multiplication_is_Associative
Provedassociativityproofwikireal-multiplication
The operation of multiplication on the set of real numbers R is associative: x * (y * z) = (x * y) * z.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Real_Multiplication_is_Associative (x y z : ℝ) : x * (y * z) = (x * y) * z := by sorry
Source