lean_workbook_plus_11130
ProvedFor we have , which is true
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_11130 : (1 : ℝ) - 1 / 2 = 1 / 2 := by sorry
Source
For we have , which is true
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_11130 : (1 : ℝ) - 1 / 2 = 1 / 2 := by sorry