Real_Addition_is_Associative
Provedassociativityproofwikireal-addition
The operation of addition 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_Addition_is_Associative (x y z : ℝ) : x + (y + z) = (x + y) + z := by sorry
Source