lean_workbook_plus_28584
ProvedFrom , we get and .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_28584 (g : ℝ → ℝ) (h : ∀ x, g (x^2) = -g x) : g 0 = 0 ∧ g 1 = 0 ∧ ∀ x, g (-x) = g x := by sorry
Source
From , we get and .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_28584 (g : ℝ → ℝ) (h : ∀ x, g (x^2) = -g x) : g 0 = 0 ∧ g 1 = 0 ∧ ∀ x, g (-x) = g x := by sorry