lean_workbook_plus_78929
ProvedWhich is which indeed fits, whatever is
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_78929 (a : ℝ) : ∀ x, (x + a) = x + a := by sorry
Source
Which is which indeed fits, whatever is
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_78929 (a : ℝ) : ∀ x, (x + a) = x + a := by sorry