Real_Addition_is_Commutative
Provedcommutativityproofwikireal-addition
The operation of addition on the set of real numbers R is commutative: x + y = y + x.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Real_Addition_is_Commutative (x y : ℝ) : x + y = y + x := by sorry
Source