Prove2Me

lean_workbook_plus_8876

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Suppose that f(1)=a f(1) = a . Then f(a)=−1 f(a) =-1 , f(−1)=−a f(-1) =-a , and f(−a)=1 f(-a) = 1 . We can see here that a a can't be 0 0 , 1 1 , or −1 -1 .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_8876  (a : ℝ)
  (f : ℝ → ℝ)
  (h₀ : f 1 = a)
  (h₁ : f a = -1)
  (h₂ : f (-1) = -a)
  (h₃ : f (-a) = 1) :
  a ≠ 0 ∧ a ≠ 1 ∧ a ≠ -1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph