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