lean_workbook_plus_40973
Opennote that:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_40973 (x : ℝ) : x^2 - x * (sin x + cos x) + sin x * cos x = (x - sin x) * (x - cos x) := by sorry
Source
note that:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_40973 (x : ℝ) : x^2 - x * (sin x + cos x) + sin x * cos x = (x - sin x) * (x - cos x) := by sorry