lean_workbook_plus_8160
Proved, which indeed fits too
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_8160 : ∃ f g : ℝ → ℝ, ∀ x, f x = -x ∧ g x = -x := by sorry
Source
, which indeed fits too
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_8160 : ∃ f g : ℝ → ℝ, ∀ x, f x = -x ∧ g x = -x := by sorry