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